Deploying to gh-pages from @ d626e59 🚀

ext/prop-eq/Mctt.Core.Soundness.LogicalRelation.Definitions.html

@@ -184,7 +184,7 @@ <h1 class="libtitle">Mctt.Core.Soundness.LogicalRelation.Definitions</h1>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Mctt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a id="9502a12eba0a165ce017e5ab88777dfd" class="idref" href="#9502a12eba0a165ce017e5ab88777dfd"><span class="id" title="binder"><span id="55ac5d9f012c888c78ecfc060ed4701b" class="id">Γ</span></span></a> <a class="idref" href="Mctt.Core.Soundness.LogicalRelation.Definitions.html#b10cb6d74e55853a85eb672ed6267907"><span class="id" title="notation">⊢</span></a> <a id="M':562" class="idref" href="#M':562"><span class="id" title="binder"><span id="M':563" class="id">M'</span></span></a> <a class="idref" href="Mctt.Core.Soundness.LogicalRelation.Definitions.html#b10cb6d74e55853a85eb672ed6267907"><span class="id" title="notation">:</span></a> <a id="A:560" class="idref" href="#A:560"><span class="id" title="binder"><span id="A:561" class="id">A</span></span></a> <a class="idref" href="Mctt.Core.Soundness.LogicalRelation.Definitions.html#b10cb6d74e55853a85eb672ed6267907"><span class="id" title="notation">®</span></a> <a class="idref" href="Mctt.Core.Semantic.Domain.html#3747efdc6ee00670493d5ab6412aedcd"><span class="id" title="notation">⇑</span></a> <a id="b:564" class="idref" href="#b:564"><span class="id" title="binder"><span id="b:565" class="id">b</span></span></a> <a id="v:566" class="idref" href="#v:566"><span class="id" title="binder"><span id="v:567" class="id">v</span></span></a> <a class="idref" href="Mctt.Core.Soundness.LogicalRelation.Definitions.html#b10cb6d74e55853a85eb672ed6267907"><span class="id" title="notation">∈</span></a> <a class="idref" href="Mctt.Core.Soundness.LogicalRelation.Definitions.html#glu_eq:460"><span class="id" title="inductive">glu_eq</span></a> <a class="idref" href="Mctt.Core.Soundness.LogicalRelation.Definitions.html#B:453"><span class="id" title="variable">B</span></a> <a class="idref" href="Mctt.Core.Soundness.LogicalRelation.Definitions.html#M:454"><span class="id" title="variable">M</span></a> <a class="idref" href="Mctt.Core.Soundness.LogicalRelation.Definitions.html#N:455"><span class="id" title="variable">N</span></a> <a class="idref" href="Mctt.Core.Soundness.LogicalRelation.Definitions.html#m:456"><span class="id" title="variable">m</span></a> <a class="idref" href="Mctt.Core.Soundness.LogicalRelation.Definitions.html#n:457"><span class="id" title="variable">n</span></a> <a class="idref" href="Mctt.Core.Soundness.LogicalRelation.Definitions.html#R:458"><span class="id" title="variable">R</span></a> <a class="idref" href="Mctt.Core.Soundness.LogicalRelation.Definitions.html#El:459"><span class="id" title="variable">El</span></a> <a class="idref" href="Mctt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a> }.<br/>
 
 <br/>
-<span class="id" title="keyword">Variant</span> <a id="eq_glu_exp_pred" class="idref" href="#eq_glu_exp_pred"><span class="id" title="inductive">eq_glu_exp_pred</span></a> <a id="i:573" class="idref" href="#i:573"><span class="id" title="binder">i</span></a> <a id="m:574" class="idref" href="#m:574"><span class="id" title="binder">m</span></a> <a id="n:575" class="idref" href="#n:575"><span class="id" title="binder">n</span></a> <a id="R:576" class="idref" href="#R:576"><span class="id" title="binder">R</span></a> <a id="P:577" class="idref" href="#P:577"><span class="id" title="binder">P</span></a> <a id="El:578" class="idref" href="#El:578"><span class="id" title="binder">El</span></a> : <a class="idref" href="Mctt.Core.Soundness.LogicalRelation.Definitions.html#:::'glu_exp_pred'"><span class="id" title="notation">glu_exp_pred</span></a> :=<br/>
+<span class="id" title="keyword">Variant</span> <a id="eq_glu_exp_pred" class="idref" href="#eq_glu_exp_pred"><span class="id" title="inductive">eq_glu_exp_pred</span></a> <a id="i:573" class="idref" href="#i:573"><span class="id" title="binder">i</span></a> <a id="m:574" class="idref" href="#m:574"><span class="id" title="binder">m</span></a> <a id="n:575" class="idref" href="#n:575"><span class="id" title="binder">n</span></a> <a id="R:576" class="idref" href="#R:576"><span class="id" title="binder">R</span></a> (<a id="P:577" class="idref" href="#P:577"><span class="id" title="binder">P</span></a> : <a class="idref" href="Mctt.Core.Soundness.LogicalRelation.Definitions.html#:::'glu_typ_pred'"><span class="id" title="notation">glu_typ_pred</span></a>) (<a id="El:578" class="idref" href="#El:578"><span class="id" title="binder">El</span></a> : <a class="idref" href="Mctt.Core.Soundness.LogicalRelation.Definitions.html#:::'glu_exp_pred'"><span class="id" title="notation">glu_exp_pred</span></a>) : <a class="idref" href="Mctt.Core.Soundness.LogicalRelation.Definitions.html#:::'glu_exp_pred'"><span class="id" title="notation">glu_exp_pred</span></a> :=<br/>
 &nbsp;&nbsp;| <a id="mk_eq_glu_exp_pred" class="idref" href="#mk_eq_glu_exp_pred"><span class="id" title="constructor">mk_eq_glu_exp_pred</span></a> :<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;`{ <a class="idref" href="Mctt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a id="52f6b2bf28556fef8f653c1b287a6fef" class="idref" href="#52f6b2bf28556fef8f653c1b287a6fef"><span class="id" title="binder"><span id="7725853e70c810c0acdcb5647236c57b" class="id">Γ</span></span></a> <a class="idref" href="Mctt.Core.Syntactic.System.Definitions.html#946b41ceb8284bcfce58d31084906f52"><span class="id" title="notation">⊢</span></a> <a id="M':585" class="idref" href="#M':585"><span class="id" title="binder"><span id="M':586" class="id">M'</span></span></a> <a class="idref" href="Mctt.Core.Syntactic.System.Definitions.html#946b41ceb8284bcfce58d31084906f52"><span class="id" title="notation">:</span></a> <a id="A:583" class="idref" href="#A:583"><span class="id" title="binder"><span id="A:584" class="id">A</span></span></a> <a class="idref" href="Mctt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a><br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Mctt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a id="d84b8ce4aa1b6bad2e4f8052fb4d4ef2" class="idref" href="#d84b8ce4aa1b6bad2e4f8052fb4d4ef2"><span class="id" title="binder"><span id="887afd1597192e7cc33807780d578f0e" class="id">Γ</span></span></a> <a class="idref" href="Mctt.Core.Syntactic.System.Definitions.html#69c002c61be42d9d1a14553e4974593f"><span class="id" title="notation">⊢</span></a> <a id="A:589" class="idref" href="#A:589"><span class="id" title="binder"><span id="A:590" class="id">A</span></span></a> <a class="idref" href="Mctt.Core.Syntactic.System.Definitions.html#69c002c61be42d9d1a14553e4974593f"><span class="id" title="notation">≈</span></a> <a class="idref" href="Mctt.Core.Syntactic.Syntax.html#Syntax_Notations.:exp:mctt_scope:'Eq'_x_x_x"><span class="id" title="notation">Eq</span></a> <a id="B:591" class="idref" href="#B:591"><span class="id" title="binder"><span id="B:592" class="id">B</span></span></a> <a id="M:593" class="idref" href="#M:593"><span class="id" title="binder"><span id="M:594" class="id">M</span></span></a> <a id="N:595" class="idref" href="#N:595"><span class="id" title="binder"><span id="N:596" class="id">N</span></span></a> <a class="idref" href="Mctt.Core.Syntactic.System.Definitions.html#69c002c61be42d9d1a14553e4974593f"><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> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a><br/>