Deploying to gh-pages from @ 8a8ceb2 🚀

ext/prop-eq/Mcltt.Core.Syntactic.CtxSub.html

@@ -50,11 +50,11 @@ <h1 class="libtitle">Mcltt.Core.Syntactic.CtxSub</h1>
 &nbsp;&nbsp;#[<span class="id" title="var">local</span>]<br/>
 &nbsp;&nbsp;<span class="id" title="keyword">Ltac</span> <span class="id" title="var">gen_ctxsub_helper_IH</span> <span class="id" title="var">ctxsub_exp_helper</span> <span class="id" title="var">ctxsub_exp_eq_helper</span> <span class="id" title="var">ctxsub_sub_helper</span> <span class="id" title="var">ctxsub_sub_eq_helper</span> <span class="id" title="var">ctxsub_subtyp_helper</span> <span class="id" title="var">H</span> :=<br/>
 &nbsp;&nbsp;<span class="id" title="keyword">match</span> <span class="id" title="keyword">type</span> <span class="id" title="keyword">of</span> <span class="id" title="var">H</span> <span class="id" title="keyword">with</span><br/>
-&nbsp;&nbsp;| <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a>?<span class="id" title="var">Γ</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#946b41ceb8284bcfce58d31084906f52"><span class="id" title="notation">⊢</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a>?<span class="id" title="var">M</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#946b41ceb8284bcfce58d31084906f52"><span class="id" title="notation">:</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a>?<span class="id" title="var">A</span> <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a> =&gt; <span class="id" title="tactic">pose</span> <span class="id" title="var">proof</span> <span class="id" title="var">ctxsub_exp_helper</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">H</span><br/>
-&nbsp;&nbsp;| <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a>?<span class="id" title="var">Γ</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#69c002c61be42d9d1a14553e4974593f"><span class="id" title="notation">⊢</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a>?<span class="id" title="var">M</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#69c002c61be42d9d1a14553e4974593f"><span class="id" title="notation">≈</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a>?<span class="id" title="var">N</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#69c002c61be42d9d1a14553e4974593f"><span class="id" title="notation">:</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a>?<span class="id" title="var">A</span> <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a> =&gt; <span class="id" title="tactic">pose</span> <span class="id" title="var">proof</span> <span class="id" title="var">ctxsub_exp_eq_helper</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">H</span><br/>
-&nbsp;&nbsp;| <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a>?<span class="id" title="var">Γ</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#fc206822ef077f61c7a4810f3d1aab63"><span class="id" title="notation">⊢</span></a><a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#fc206822ef077f61c7a4810f3d1aab63"><span class="id" title="notation">s</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a>?σ <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#fc206822ef077f61c7a4810f3d1aab63"><span class="id" title="notation">:</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a>?<span class="id" title="var">Δ</span> <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a> =&gt; <span class="id" title="tactic">pose</span> <span class="id" title="var">proof</span> <span class="id" title="var">ctxsub_sub_helper</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">H</span><br/>
-&nbsp;&nbsp;| <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a>?<span class="id" title="var">Γ</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#9d3593e23dab0912c81fcf20fe94e371"><span class="id" title="notation">⊢</span></a><a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#9d3593e23dab0912c81fcf20fe94e371"><span class="id" title="notation">s</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a>?σ <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#9d3593e23dab0912c81fcf20fe94e371"><span class="id" title="notation">≈</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a>?τ <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#9d3593e23dab0912c81fcf20fe94e371"><span class="id" title="notation">:</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a>?<span class="id" title="var">Δ</span> <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a> =&gt; <span class="id" title="tactic">pose</span> <span class="id" title="var">proof</span> <span class="id" title="var">ctxsub_sub_eq_helper</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">H</span><br/>
-&nbsp;&nbsp;| <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a>?<span class="id" title="var">Γ</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#1ebf0ff69b866207c2e2c9dfeeb72b65"><span class="id" title="notation">⊢</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a>?<span class="id" title="var">M</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#1ebf0ff69b866207c2e2c9dfeeb72b65"><span class="id" title="notation">⊆</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#c7c4058a6f257008261812cf0ba20ccd"><span class="id" title="notation">~</span></a>?<span class="id" title="var">M'</span> <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a> =&gt; <span class="id" title="tactic">pose</span> <span class="id" title="var">proof</span> <span class="id" title="var">ctxsub_subtyp_helper</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">H</span><br/>
+&nbsp;&nbsp;| <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ad7c00f8799eccf810496ae461d2734e"><span class="id" title="notation">^</span></a>?<span class="id" title="var">Γ</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#946b41ceb8284bcfce58d31084906f52"><span class="id" title="notation">⊢</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ad7c00f8799eccf810496ae461d2734e"><span class="id" title="notation">^</span></a>?<span class="id" title="var">M</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#946b41ceb8284bcfce58d31084906f52"><span class="id" title="notation">:</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ad7c00f8799eccf810496ae461d2734e"><span class="id" title="notation">^</span></a>?<span class="id" title="var">A</span> <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a> =&gt; <span class="id" title="tactic">pose</span> <span class="id" title="var">proof</span> <span class="id" title="var">ctxsub_exp_helper</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">H</span><br/>
+&nbsp;&nbsp;| <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ad7c00f8799eccf810496ae461d2734e"><span class="id" title="notation">^</span></a>?<span class="id" title="var">Γ</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#69c002c61be42d9d1a14553e4974593f"><span class="id" title="notation">⊢</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ad7c00f8799eccf810496ae461d2734e"><span class="id" title="notation">^</span></a>?<span class="id" title="var">M</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#69c002c61be42d9d1a14553e4974593f"><span class="id" title="notation">≈</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ad7c00f8799eccf810496ae461d2734e"><span class="id" title="notation">^</span></a>?<span class="id" title="var">N</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#69c002c61be42d9d1a14553e4974593f"><span class="id" title="notation">:</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ad7c00f8799eccf810496ae461d2734e"><span class="id" title="notation">^</span></a>?<span class="id" title="var">A</span> <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a> =&gt; <span class="id" title="tactic">pose</span> <span class="id" title="var">proof</span> <span class="id" title="var">ctxsub_exp_eq_helper</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">H</span><br/>
+&nbsp;&nbsp;| <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ad7c00f8799eccf810496ae461d2734e"><span class="id" title="notation">^</span></a>?<span class="id" title="var">Γ</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#fc206822ef077f61c7a4810f3d1aab63"><span class="id" title="notation">⊢</span></a><a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#fc206822ef077f61c7a4810f3d1aab63"><span class="id" title="notation">s</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ad7c00f8799eccf810496ae461d2734e"><span class="id" title="notation">^</span></a>?σ <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#fc206822ef077f61c7a4810f3d1aab63"><span class="id" title="notation">:</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ad7c00f8799eccf810496ae461d2734e"><span class="id" title="notation">^</span></a>?<span class="id" title="var">Δ</span> <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a> =&gt; <span class="id" title="tactic">pose</span> <span class="id" title="var">proof</span> <span class="id" title="var">ctxsub_sub_helper</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">H</span><br/>
+&nbsp;&nbsp;| <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ad7c00f8799eccf810496ae461d2734e"><span class="id" title="notation">^</span></a>?<span class="id" title="var">Γ</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#9d3593e23dab0912c81fcf20fe94e371"><span class="id" title="notation">⊢</span></a><a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#9d3593e23dab0912c81fcf20fe94e371"><span class="id" title="notation">s</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ad7c00f8799eccf810496ae461d2734e"><span class="id" title="notation">^</span></a>?σ <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#9d3593e23dab0912c81fcf20fe94e371"><span class="id" title="notation">≈</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ad7c00f8799eccf810496ae461d2734e"><span class="id" title="notation">^</span></a>?τ <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#9d3593e23dab0912c81fcf20fe94e371"><span class="id" title="notation">:</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ad7c00f8799eccf810496ae461d2734e"><span class="id" title="notation">^</span></a>?<span class="id" title="var">Δ</span> <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a> =&gt; <span class="id" title="tactic">pose</span> <span class="id" title="var">proof</span> <span class="id" title="var">ctxsub_sub_eq_helper</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">H</span><br/>
+&nbsp;&nbsp;| <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ad7c00f8799eccf810496ae461d2734e"><span class="id" title="notation">^</span></a>?<span class="id" title="var">Γ</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#1ebf0ff69b866207c2e2c9dfeeb72b65"><span class="id" title="notation">⊢</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ad7c00f8799eccf810496ae461d2734e"><span class="id" title="notation">^</span></a>?<span class="id" title="var">M</span> <a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#1ebf0ff69b866207c2e2c9dfeeb72b65"><span class="id" title="notation">⊆</span></a> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ad7c00f8799eccf810496ae461d2734e"><span class="id" title="notation">^</span></a>?<span class="id" title="var">M'</span> <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a> =&gt; <span class="id" title="tactic">pose</span> <span class="id" title="var">proof</span> <span class="id" title="var">ctxsub_subtyp_helper</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">H</span><br/>
 &nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
 
 <br/>