Deploying to gh-pages from @ 0507289 🚀

ext/prop-eq/Mctt.Core.Soundness.FunctionCases.html

@@ -80,12 +80,7 @@ <h1 class="libtitle">Mctt.Core.Soundness.FunctionCases</h1>
 &nbsp;&nbsp;<span class="id" title="tactic">intros</span>.<br/>
 &nbsp;&nbsp;<span class="id" title="tactic">assert</span> <a class="idref" href="Mctt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a id="6c47ab78a6e5e3bed39dd19a10492bea" class="idref" href="#6c47ab78a6e5e3bed39dd19a10492bea"><span class="id" title="binder"><span id="7fe7ff094807f92f8c1b51b6b621c026" class="id"><span id="deb9f131fb74ffe527b919b3a7916da1" class="id"><span id="07c2048c9fea60edbbf1921003ad043d" class="id">Δ</span></span></span></span></a> <a class="idref" href="Mctt.Core.Syntactic.System.Definitions.html#fc206822ef077f61c7a4810f3d1aab63"><span class="id" title="notation">⊢</span></a><a class="idref" href="Mctt.Core.Syntactic.System.Definitions.html#fc206822ef077f61c7a4810f3d1aab63"><span class="id" title="notation">s</span></a> <a id="5f0c308148843d82eda723a5f1795efa" class="idref" href="#5f0c308148843d82eda723a5f1795efa"><span class="id" title="binder"><span id="a6e4d683e55bf2b470c0972aeb840aae" class="id"><span id="9d63b48741968edd9f9abc0327a8bb16" class="id"><span id="6abb26837f133469b778e4847557de62" class="id">σ</span></span></span></span></a> <a class="idref" href="Mctt.Core.Syntactic.System.Definitions.html#fc206822ef077f61c7a4810f3d1aab63"><span class="id" title="notation">:</span></a> <a id="a3659dace81f0834ea0666465bcde48d" class="idref" href="#a3659dace81f0834ea0666465bcde48d"><span class="id" title="binder"><span id="483c47e7100adec85d58e3dde43d0c71" class="id"><span id="ac5d8d48b7be54da12b37241ba2f5040" class="id"><span id="d60cca09333596614699de21d7139a5f" class="id">Γ</span></span></span></span></a> <a class="idref" href="Mctt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a> <span class="id" title="tactic">by</span> <span class="id" title="var">mauto</span> 4.<br/>
 &nbsp;&nbsp;<span class="id" title="tactic">split</span>; <span class="id" title="var">mauto</span> 3.<br/>
-&nbsp;&nbsp;<span class="id" title="var">destruct_glu_rel_exp_with_sub</span>.<br/>
-&nbsp;&nbsp;<span class="id" title="var">simplify_evals</span>.<br/>
-&nbsp;&nbsp;<span class="id" title="var">match_by_head</span> <a class="idref" href="Mctt.Core.Soundness.LogicalRelation.Definitions.html#glu_univ_elem"><span class="id" title="definition">glu_univ_elem</span></a> <span class="id" title="keyword">ltac</span>:(<span class="id" title="keyword">fun</span> <span class="id" title="var">H</span> =&gt; <span class="id" title="var">directed</span> <span class="id" title="var">invert_glu_univ_elem</span> <span class="id" title="var">H</span>).<br/>
-&nbsp;&nbsp;<span class="id" title="var">handle_functional_glu_univ_elem</span>.<br/>
-&nbsp;&nbsp;<span class="id" title="tactic">unfold</span> <a class="idref" href="Mctt.Core.Soundness.LogicalRelation.Definitions.html#univ_glu_exp_pred'"><span class="id" title="definition">univ_glu_exp_pred'</span></a> <span class="id" title="tactic">in</span> *.<br/>
-&nbsp;&nbsp;<span class="id" title="var">destruct_conjs</span>.<br/>
+&nbsp;&nbsp;<span class="id" title="var">apply_glu_rel_judge</span>.<br/>
 &nbsp;&nbsp;<span class="id" title="tactic">rename</span> <span class="id" title="var">m</span> <span class="id" title="var">into</span> <span class="id" title="var">a</span>.<br/>
 &nbsp;&nbsp;<span class="id" title="tactic">assert</span> <a class="idref" href="Mctt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a id="233c8f5f4890e0afc448c71b7d21a4cd" class="idref" href="#233c8f5f4890e0afc448c71b7d21a4cd"><span class="id" title="binder"><span id="92d13f9ec58cd846d6d01f1493fbea43" class="id"><span id="541f685d9f55386c1e35d14997e60f9c" class="id"><span id="4528c44f6a9a8b29b3b50e8b6265970b" class="id">Γ</span></span></span></span></a> <a class="idref" href="Mctt.Core.Completeness.LogicalRelation.Definitions.html#3c1b6b654dd5c53132870fe8b8af59b4"><span class="id" title="notation">⊨</span></a> <a class="idref" href="Mctt.Core.Syntactic.Syntax.html#78f41cc0c59f179d49e1957fedd82d6e"><span class="id" title="notation">Π</span></a> <a id="A:199" class="idref" href="#A:199"><span class="id" title="binder"><span id="A:200" class="id"><span id="A:205" class="id"><span id="A:206" class="id">A</span></span></span></span></a> <a id="B:201" class="idref" href="#B:201"><span class="id" title="binder"><span id="B:202" class="id"><span id="B:207" class="id"><span id="B:208" class="id">B</span></span></span></span></a> <a class="idref" href="Mctt.Core.Completeness.LogicalRelation.Definitions.html#3c1b6b654dd5c53132870fe8b8af59b4"><span class="id" title="notation">:</span></a> <a class="idref" href="Mctt.Core.Syntactic.Syntax.html#efd901996cb10f37561c83ae2288c419"><span class="id" title="notation">Type@i</span></a> <a class="idref" href="Mctt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a> <span class="id" title="keyword">as</span> [<span class="id" title="var">env_relΓ</span>]%<a class="idref" href="Mctt.Core.Completeness.UniverseCases.html#rel_exp_of_typ_inversion1"><span class="id" title="lemma">rel_exp_of_typ_inversion1</span></a> <span class="id" title="tactic">by</span> <span class="id" title="var">mauto</span> 3 <span class="id" title="keyword">using</span> <a class="idref" href="Mctt.Core.Completeness.FundamentalTheorem.html#completeness_fundamental_exp"><span class="id" title="lemma">completeness_fundamental_exp</span></a>.<br/>
 &nbsp;&nbsp;<span class="id" title="tactic">assert</span> <a class="idref" href="Mctt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a id="dcc71771dbbab30de93aa8a879cf7dbb" class="idref" href="#dcc71771dbbab30de93aa8a879cf7dbb"><span class="id" title="binder"><span id="5a8dc7e3a6d5df1731c8d68c52569ee1" class="id"><span id="90404e84950a6f59c1bcc9fdaea56cc0" class="id"><span id="b049477b434d1524f13e35137a161630" class="id">Γ</span></span></span></span></a><a class="idref" href="Mctt.Core.Syntactic.Syntax.html#545d14d3749e4214500beb453d7ad50f"><span class="id" title="notation">,</span></a> <a id="A:209" class="idref" href="#A:209"><span class="id" title="binder"><span id="A:210" class="id"><span id="A:215" class="id"><span id="A:216" class="id">A</span></span></span></span></a> <a class="idref" href="Mctt.Core.Completeness.LogicalRelation.Definitions.html#3c1b6b654dd5c53132870fe8b8af59b4"><span class="id" title="notation">⊨</span></a> <a id="B:213" class="idref" href="#B:213"><span class="id" title="binder"><span id="B:214" class="id"><span id="B:219" class="id"><span id="B:220" class="id">B</span></span></span></span></a> <a class="idref" href="Mctt.Core.Completeness.LogicalRelation.Definitions.html#3c1b6b654dd5c53132870fe8b8af59b4"><span class="id" title="notation">:</span></a> <a class="idref" href="Mctt.Core.Syntactic.Syntax.html#efd901996cb10f37561c83ae2288c419"><span class="id" title="notation">Type@i</span></a> <a class="idref" href="Mctt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a> <span class="id" title="keyword">as</span> [<span class="id" title="var">env_relΓA</span>]%<a class="idref" href="Mctt.Core.Completeness.UniverseCases.html#rel_exp_of_typ_inversion1"><span class="id" title="lemma">rel_exp_of_typ_inversion1</span></a> <span class="id" title="tactic">by</span> <span class="id" title="var">mauto</span> 3 <span class="id" title="keyword">using</span> <a class="idref" href="Mctt.Core.Completeness.FundamentalTheorem.html#completeness_fundamental_exp"><span class="id" title="lemma">completeness_fundamental_exp</span></a>.<br/>