Deploying to gh-pages from @ 8a8bde5 🚀

Mcltt.Core.Completeness.TermStructureCases.html

@@ -53,8 +53,8 @@ <h1 class="libtitle">Mcltt.Core.Completeness.TermStructureCases</h1>
 &nbsp;&nbsp;(<span class="id" title="var">on_all_hyp</span>: <span class="id" title="var">destruct_rel_by_assumption</span> <span class="id" title="var">env_relΓ</span>).<br/>
 &nbsp;&nbsp;<span class="id" title="var">handle_per_univ_elem_irrel</span>.<br/>
 &nbsp;&nbsp;<span class="id" title="keyword">match</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
-&nbsp;&nbsp;| <span class="id" title="var">_</span>: <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a class="idref" href="Mcltt.Core.Semantic.Evaluation.Definitions.html#fb4372a57c3d066845b17ca7d0234d9f"><span class="id" title="notation">⟦</span></a> <a id="976ecaa1329e69582a26aa858b5e636c" class="idref" href="#976ecaa1329e69582a26aa858b5e636c"><span class="id" title="binder"><span id="280fe6e9a98af7df6c57e9f4080a26e0" class="id"><span id="afbe70ee4da91bd9a61766970a62c153" class="id"><span id="e301eb36a877cd02cbb5965c6e966e14" class="id">σ</span></span></span></span></a> <a class="idref" href="Mcltt.Core.Semantic.Evaluation.Definitions.html#fb4372a57c3d066845b17ca7d0234d9f"><span class="id" title="notation">⟧</span></a><a class="idref" href="Mcltt.Core.Semantic.Evaluation.Definitions.html#fb4372a57c3d066845b17ca7d0234d9f"><span class="id" title="notation">s</span></a> <a id="60121a901814d5edce33b68edc4ef496" class="idref" href="#60121a901814d5edce33b68edc4ef496"><span class="id" title="binder"><span id="4531680360bc625b2bb8230693d97665" class="id"><span id="59afde9a8c5674ac0696932d63f1f0d2" class="id"><span id="67f3a7da2c49974781df82d45ce07ab1" class="id">ρ</span></span></span></span></a> <a class="idref" href="Mcltt.Core.Semantic.Evaluation.Definitions.html#fb4372a57c3d066845b17ca7d0234d9f"><span class="id" title="notation">↘</span></a> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#1fb14ce35194a2309d4e68e8326d78de"><span class="id" title="notation">~</span></a>?ρ0 <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a>,<br/>
-&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">_</span>: <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a class="idref" href="Mcltt.Core.Semantic.Evaluation.Definitions.html#fb4372a57c3d066845b17ca7d0234d9f"><span class="id" title="notation">⟦</span></a> <a id="e93730f81c7d57a53384de85ec2132b9" class="idref" href="#e93730f81c7d57a53384de85ec2132b9"><span class="id" title="binder"><span id="430eb15c7314e2ebbce013f4e023cc44" class="id"><span id="5cdb643423f970505cbe86645593e303" class="id"><span id="aabbb3071490a3e89c35c54fc4d8b7c4" class="id">σ</span></span></span></span></a> <a class="idref" href="Mcltt.Core.Semantic.Evaluation.Definitions.html#fb4372a57c3d066845b17ca7d0234d9f"><span class="id" title="notation">⟧</span></a><a class="idref" href="Mcltt.Core.Semantic.Evaluation.Definitions.html#fb4372a57c3d066845b17ca7d0234d9f"><span class="id" title="notation">s</span></a> <a id="a0822ca16043e6dba047d8a8cadbaf06" class="idref" href="#a0822ca16043e6dba047d8a8cadbaf06"><span class="id" title="binder"><span id="4361f3d4c80467107716c98601e8da39" class="id"><span id="348c0df51bf56ebd78f126801fe8b382" class="id"><span id="062faac3711fdebefc116ee1cc1fc99c" class="id">ρ'</span></span></span></span></a> <a class="idref" href="Mcltt.Core.Semantic.Evaluation.Definitions.html#fb4372a57c3d066845b17ca7d0234d9f"><span class="id" title="notation">↘</span></a> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#1fb14ce35194a2309d4e68e8326d78de"><span class="id" title="notation">~</span></a>?ρ'0 <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a> |- <span class="id" title="var">_</span> =&gt;<br/>
+&nbsp;&nbsp;| <span class="id" title="var">_</span>: <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a class="idref" href="Mcltt.Core.Semantic.Evaluation.Definitions.html#fb4372a57c3d066845b17ca7d0234d9f"><span class="id" title="notation">⟦</span></a> <a id="976ecaa1329e69582a26aa858b5e636c" class="idref" href="#976ecaa1329e69582a26aa858b5e636c"><span class="id" title="binder"><span id="280fe6e9a98af7df6c57e9f4080a26e0" class="id"><span id="afbe70ee4da91bd9a61766970a62c153" class="id"><span id="e301eb36a877cd02cbb5965c6e966e14" class="id">σ</span></span></span></span></a> <a class="idref" href="Mcltt.Core.Semantic.Evaluation.Definitions.html#fb4372a57c3d066845b17ca7d0234d9f"><span class="id" title="notation">⟧</span></a><a class="idref" href="Mcltt.Core.Semantic.Evaluation.Definitions.html#fb4372a57c3d066845b17ca7d0234d9f"><span class="id" title="notation">s</span></a> <a id="60121a901814d5edce33b68edc4ef496" class="idref" href="#60121a901814d5edce33b68edc4ef496"><span class="id" title="binder"><span id="4531680360bc625b2bb8230693d97665" class="id"><span id="59afde9a8c5674ac0696932d63f1f0d2" class="id"><span id="67f3a7da2c49974781df82d45ce07ab1" class="id">ρ</span></span></span></span></a> <a class="idref" href="Mcltt.Core.Semantic.Evaluation.Definitions.html#fb4372a57c3d066845b17ca7d0234d9f"><span class="id" title="notation">↘</span></a> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#6a42f9250592fab402cdf9f7b4d3f15c"><span class="id" title="notation">^</span></a>?ρ0 <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a>,<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">_</span>: <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a class="idref" href="Mcltt.Core.Semantic.Evaluation.Definitions.html#fb4372a57c3d066845b17ca7d0234d9f"><span class="id" title="notation">⟦</span></a> <a id="e93730f81c7d57a53384de85ec2132b9" class="idref" href="#e93730f81c7d57a53384de85ec2132b9"><span class="id" title="binder"><span id="430eb15c7314e2ebbce013f4e023cc44" class="id"><span id="5cdb643423f970505cbe86645593e303" class="id"><span id="aabbb3071490a3e89c35c54fc4d8b7c4" class="id">σ</span></span></span></span></a> <a class="idref" href="Mcltt.Core.Semantic.Evaluation.Definitions.html#fb4372a57c3d066845b17ca7d0234d9f"><span class="id" title="notation">⟧</span></a><a class="idref" href="Mcltt.Core.Semantic.Evaluation.Definitions.html#fb4372a57c3d066845b17ca7d0234d9f"><span class="id" title="notation">s</span></a> <a id="a0822ca16043e6dba047d8a8cadbaf06" class="idref" href="#a0822ca16043e6dba047d8a8cadbaf06"><span class="id" title="binder"><span id="4361f3d4c80467107716c98601e8da39" class="id"><span id="348c0df51bf56ebd78f126801fe8b382" class="id"><span id="062faac3711fdebefc116ee1cc1fc99c" class="id">ρ'</span></span></span></span></a> <a class="idref" href="Mcltt.Core.Semantic.Evaluation.Definitions.html#fb4372a57c3d066845b17ca7d0234d9f"><span class="id" title="notation">↘</span></a> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#6a42f9250592fab402cdf9f7b4d3f15c"><span class="id" title="notation">^</span></a>?ρ'0 <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a> |- <span class="id" title="var">_</span> =&gt;<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rename</span> ρ0 <span class="id" title="var">into</span> ρσ;<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rename</span> ρ'0 <span class="id" title="var">into</span> ρ'σ<br/>
 &nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>