From b02f8abe5fbd98f20b9e90ee222df59ba05c77f7 Mon Sep 17 00:00:00 2001
From: Ailrun <jjc9310@gmail.com>
Date: Wed, 18 Sep 2024 01:09:05 +0000
Subject: [PATCH] =?UTF-8?q?Deploying=20to=20gh-pages=20from=20@=20Beluga-l?=
 =?UTF-8?q?ang/McLTT@f5c2bb599220709c9d6b2dc58c336ea5715724b7=20?=
 =?UTF-8?q?=F0=9F=9A=80?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Mcltt.Core.Semantic.PER.Definitions.html      |  45 +++++--
 ....Soundness.LogicalRelation.CoreLemmas.html |  10 +-
 ...Core.Soundness.LogicalRelation.Lemmas.html |  10 +-
 Mcltt.Core.Syntactic.Syntax.html              |  13 +-
 Mcltt.Core.Syntactic.System.Lemmas.html       |  12 +-
 Mcltt.Frontend.Elaborator.html                |   2 +-
 Mcltt.LibTactics.html                         |  10 +-
 toc.html                                      | 121 +++---------------
 8 files changed, 79 insertions(+), 144 deletions(-)

diff --git a/Mcltt.Core.Semantic.PER.Definitions.html b/Mcltt.Core.Semantic.PER.Definitions.html
index af6a698..110fe19 100644
--- a/Mcltt.Core.Semantic.PER.Definitions.html
+++ b/Mcltt.Core.Semantic.PER.Definitions.html
@@ -57,7 +57,7 @@ <h1 class="libtitle">Mcltt.Core.Semantic.PER.Definitions</h1>
 </div>
 
 <div class="doc">
-<a id="lab1"></a><h2 class="section">Helper Bundles</h2>
+<a id="lab1"></a><h3 class="section">Helper Bundles</h3>
  Related modulo evaluation 
 </div>
 <div class="code">
@@ -84,7 +84,7 @@ <h1 class="libtitle">Mcltt.Core.Semantic.PER.Definitions</h1>
 </div>
 
 <div class="doc">
-<a id="lab2"></a><h2 class="section">(Some Elements of) PER Lattice</h2>
+<a id="lab2"></a><h3 class="section">(Some Elements of) PER Lattice</h3>
 
 </div>
 <div class="code">
@@ -142,7 +142,8 @@ <h1 class="libtitle">Mcltt.Core.Semantic.PER.Definitions</h1>
 </div>
 
 <div class="doc">
-<a id="lab3"></a><h2 class="section">Universe/Element PER Definition</h2>
+<a id="lab3"></a><h1 class="section">Universe/Element PER</h1>
+<a id="lab4"></a><h2 class="section">Universe/Element PER Definition</h2>
 
 </div>
 <div class="code">
@@ -261,7 +262,7 @@ <h1 class="libtitle">Mcltt.Core.Semantic.PER.Definitions</h1>
 </div>
 
 <div class="doc">
-<a id="lab4"></a><h2 class="section">Universe/Element PER Induction Principle</h2>
+<a id="lab5"></a><h2 class="section">Universe/Element PER Induction Principle</h2>
 
 </div>
 <div class="code">
@@ -319,6 +320,15 @@ <h1 class="libtitle">Mcltt.Core.Semantic.PER.Definitions</h1>
 <br/>
 <span class="id" title="keyword">Reserved Notation</span> &quot;'Sub' a &lt;: b 'at' i" (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">judg</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 90, <span class="id" title="var">a</span> <span class="id" title="var">custom</span> <span class="id" title="var">domain</span>, <span class="id" title="var">b</span> <span class="id" title="var">custom</span> <span class="id" title="var">domain</span>, <span class="id" title="var">i</span> <span class="id" title="keyword">constr</span>).<br/>
 
+<br/>
+</div>
+
+<div class="doc">
+<a id="lab6"></a><h1 class="section">Universe Subtyping</h1>
+
+</div>
+<div class="code">
+
 <br/>
 <span class="id" title="keyword">Inductive</span> <a id="per_subtyp" class="idref" href="#per_subtyp"><span class="id" title="definition, inductive"><span id="per_subtyp_ind" class="id"><span id="per_subtyp_sind" class="id">per_subtyp</span></span></span></a> : <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</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> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#domain"><span class="id" title="inductive">domain</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> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#domain"><span class="id" title="inductive">domain</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> <span class="id" title="keyword">Prop</span> :=<br/>
 | <a id="per_subtyp_neut" class="idref" href="#per_subtyp_neut"><span class="id" title="constructor">per_subtyp_neut</span></a> :<br/>
@@ -347,15 +357,6 @@ <h1 class="libtitle">Mcltt.Core.Semantic.PER.Definitions</h1>
 #[<span class="id" title="var">export</span>]<br/>
 &nbsp;<span class="id" title="keyword">Hint</span> <span class="id" title="keyword">Constructors</span> <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#per_subtyp"><span class="id" title="inductive">per_subtyp</span></a> : <span class="id" title="var">mcltt</span>.<br/>
 
-<br/>
-</div>
-
-<div class="doc">
-<a id="lab5"></a><h2 class="section">Context/Environment PER</h2>
-
-</div>
-<div class="code">
-
 <br/>
 <span class="id" title="keyword">Definition</span> <a id="rel_typ" class="idref" href="#rel_typ"><span class="id" title="definition">rel_typ</span></a> <a id="i:733" class="idref" href="#i:733"><span class="id" title="binder">i</span></a> <a id="A:734" class="idref" href="#A:734"><span class="id" title="binder">A</span></a> <a id="cb4b3ec485a1b3943d8b917ebd8a0d3e" class="idref" href="#cb4b3ec485a1b3943d8b917ebd8a0d3e"><span class="id" title="binder">ρ</span></a> <a id="A':736" class="idref" href="#A':736"><span class="id" title="binder">A'</span></a> <a id="48375aae3cd0e421cd716a4fe1341378" class="idref" href="#48375aae3cd0e421cd716a4fe1341378"><span class="id" title="binder">ρ'</span></a> <a id="R':738" class="idref" href="#R':738"><span class="id" title="binder">R'</span></a> := <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#rel_mod_eval"><span class="id" title="inductive">rel_mod_eval</span></a> (<a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#per_univ_elem"><span class="id" title="definition">per_univ_elem</span></a> <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#i:733"><span class="id" title="variable">i</span></a>) <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#A:734"><span class="id" title="variable">A</span></a> <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#cb4b3ec485a1b3943d8b917ebd8a0d3e"><span class="id" title="variable">ρ</span></a> <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#A':736"><span class="id" title="variable">A'</span></a> <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#48375aae3cd0e421cd716a4fe1341378"><span class="id" title="variable">ρ'</span></a> <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#R':738"><span class="id" title="variable">R'</span></a>.<br/>
 <span class="id" title="keyword">Arguments</span> <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#rel_typ"><span class="id" title="definition">rel_typ</span></a> <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">_</span> <span class="id" title="var">_</span> /.<br/>
@@ -364,6 +365,15 @@ <h1 class="libtitle">Mcltt.Core.Semantic.PER.Definitions</h1>
 #[<span class="id" title="var">export</span>]<br/>
 <span class="id" title="keyword">Hint</span> <span class="id" title="keyword">Unfold</span> <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#rel_typ"><span class="id" title="definition">rel_typ</span></a> : <span class="id" title="var">mcltt</span>.<br/>
 
+<br/>
+</div>
+
+<div class="doc">
+<a id="lab7"></a><h1 class="section">Context/Environment PER</h1>
+
+</div>
+<div class="code">
+
 <br/>
 <span class="id" title="keyword">Inductive</span> <a id="per_ctx_env" class="idref" href="#per_ctx_env"><span class="id" title="definition, inductive"><span id="per_ctx_env_ind" class="id"><span id="per_ctx_env_sind" class="id">per_ctx_env</span></span></span></a> : <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Relations.Relation_Definitions.html#relation"><span class="id" title="definition">relation</span></a> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#:::'env'"><span class="id" title="notation">env</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> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ctx"><span class="id" title="abbreviation">ctx</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> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ctx"><span class="id" title="abbreviation">ctx</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> <span class="id" title="keyword">Prop</span> :=<br/>
 | <a id="per_ctx_env_nil" class="idref" href="#per_ctx_env_nil"><span class="id" title="constructor">per_ctx_env_nil</span></a> :<br/>
@@ -397,6 +407,15 @@ <h1 class="libtitle">Mcltt.Core.Semantic.PER.Definitions</h1>
 <br/>
 <span class="id" title="keyword">Reserved Notation</span> &quot;'SubE' Γ &lt;: Δ" (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">judg</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 90, <span class="id" title="var">Γ</span> <span class="id" title="var">custom</span> <span class="id" title="var">exp</span>, <span class="id" title="var">Δ</span> <span class="id" title="var">custom</span> <span class="id" title="var">exp</span>).<br/>
 
+<br/>
+</div>
+
+<div class="doc">
+<a id="lab8"></a><h1 class="section">Context Subtyping</h1>
+
+</div>
+<div class="code">
+
 <br/>
 <span class="id" title="keyword">Inductive</span> <a id="per_ctx_subtyp" class="idref" href="#per_ctx_subtyp"><span class="id" title="definition, inductive"><span id="per_ctx_subtyp_ind" class="id"><span id="per_ctx_subtyp_sind" class="id">per_ctx_subtyp</span></span></span></a> : <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ctx"><span class="id" title="abbreviation">ctx</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> <a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#ctx"><span class="id" title="abbreviation">ctx</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> <span class="id" title="keyword">Prop</span> :=<br/>
 | <a id="per_ctx_subtyp_nil" class="idref" href="#per_ctx_subtyp_nil"><span class="id" title="constructor">per_ctx_subtyp_nil</span></a> :<br/>
diff --git a/Mcltt.Core.Soundness.LogicalRelation.CoreLemmas.html b/Mcltt.Core.Soundness.LogicalRelation.CoreLemmas.html
index 6b8df42..eb13c97 100644
--- a/Mcltt.Core.Soundness.LogicalRelation.CoreLemmas.html
+++ b/Mcltt.Core.Soundness.LogicalRelation.CoreLemmas.html
@@ -495,7 +495,7 @@ <h1 class="libtitle">Mcltt.Core.Soundness.LogicalRelation.CoreLemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab6"></a><h2 class="section">Simple Morphism instance for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_univ_elem"><span class="id" title="definition">glu_univ_elem</span></a></span></h2>
+<a id="lab9"></a><h3 class="section">Simple Morphism instance for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_univ_elem"><span class="id" title="definition">glu_univ_elem</span></a></span></h3>
 
 </div>
 <div class="code">
@@ -512,7 +512,7 @@ <h1 class="libtitle">Mcltt.Core.Soundness.LogicalRelation.CoreLemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab7"></a><h2 class="section">Morphism instances for <span class="inlinecode"><span class="id" title="var">neut_glu_</span>*<span class="id" title="var">_pred</span></span>s</h2>
+<a id="lab10"></a><h3 class="section">Morphism instances for <span class="inlinecode"><span class="id" title="var">neut_glu_</span>*<span class="id" title="var">_pred</span></span>s</h3>
 
 </div>
 <div class="code">
@@ -552,7 +552,7 @@ <h1 class="libtitle">Mcltt.Core.Soundness.LogicalRelation.CoreLemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab8"></a><h2 class="section">Morphism instances for <span class="inlinecode"><span class="id" title="var">pi_glu_</span>*<span class="id" title="var">_pred</span></span>s</h2>
+<a id="lab11"></a><h3 class="section">Morphism instances for <span class="inlinecode"><span class="id" title="var">pi_glu_</span>*<span class="id" title="var">_pred</span></span>s</h3>
 
 </div>
 <div class="code">
@@ -782,7 +782,7 @@ <h1 class="libtitle">Mcltt.Core.Soundness.LogicalRelation.CoreLemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab9"></a><h2 class="section">Morphism instances for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_univ_elem"><span class="id" title="definition">glu_univ_elem</span></a></span></h2>
+<a id="lab12"></a><h3 class="section">Morphism instances for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_univ_elem"><span class="id" title="definition">glu_univ_elem</span></a></span></h3>
 
 </div>
 <div class="code">
@@ -1094,7 +1094,7 @@ <h1 class="libtitle">Mcltt.Core.Soundness.LogicalRelation.CoreLemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab10"></a><h2 class="section">Simple Morphism instance for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_ctx_env"><span class="id" title="inductive">glu_ctx_env</span></a></span></h2>
+<a id="lab13"></a><h3 class="section">Simple Morphism instance for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_ctx_env"><span class="id" title="inductive">glu_ctx_env</span></a></span></h3>
 
 </div>
 <div class="code">
diff --git a/Mcltt.Core.Soundness.LogicalRelation.Lemmas.html b/Mcltt.Core.Soundness.LogicalRelation.Lemmas.html
index 937ff56..e6d45db 100644
--- a/Mcltt.Core.Soundness.LogicalRelation.Lemmas.html
+++ b/Mcltt.Core.Soundness.LogicalRelation.Lemmas.html
@@ -633,7 +633,7 @@ <h1 class="libtitle">Mcltt.Core.Soundness.LogicalRelation.Lemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab11"></a><h2 class="section">Lemmas for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_rel_typ_with_sub"><span class="id" title="inductive">glu_rel_typ_with_sub</span></a></span> and <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_rel_exp_with_sub"><span class="id" title="inductive">glu_rel_exp_with_sub</span></a></span></h2>
+<a id="lab14"></a><h3 class="section">Lemmas for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_rel_typ_with_sub"><span class="id" title="inductive">glu_rel_typ_with_sub</span></a></span> and <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_rel_exp_with_sub"><span class="id" title="inductive">glu_rel_exp_with_sub</span></a></span></h3>
 
 </div>
 <div class="code">
@@ -761,7 +761,7 @@ <h1 class="libtitle">Mcltt.Core.Soundness.LogicalRelation.Lemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab12"></a><h2 class="section">Lemmas for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_ctx_env"><span class="id" title="inductive">glu_ctx_env</span></a></span></h2>
+<a id="lab15"></a><h3 class="section">Lemmas for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_ctx_env"><span class="id" title="inductive">glu_ctx_env</span></a></span></h3>
 
 </div>
 <div class="code">
@@ -1167,7 +1167,7 @@ <h1 class="libtitle">Mcltt.Core.Soundness.LogicalRelation.Lemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab13"></a><h2 class="section">Tactics for <span class="inlinecode"><span class="id" title="var">glu_rel_</span>*</span></h2>
+<a id="lab16"></a><h3 class="section">Tactics for <span class="inlinecode"><span class="id" title="var">glu_rel_</span>*</span></h3>
 
 </div>
 <div class="code">
@@ -1215,7 +1215,7 @@ <h1 class="libtitle">Mcltt.Core.Soundness.LogicalRelation.Lemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab14"></a><h2 class="section">Lemmas about <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_rel_exp"><span class="id" title="definition">glu_rel_exp</span></a></span></h2>
+<a id="lab17"></a><h3 class="section">Lemmas about <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_rel_exp"><span class="id" title="definition">glu_rel_exp</span></a></span></h3>
 
 </div>
 <div class="code">
@@ -1297,7 +1297,7 @@ <h1 class="libtitle">Mcltt.Core.Soundness.LogicalRelation.Lemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab15"></a><h2 class="section">Lemmas about <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_rel_sub"><span class="id" title="definition">glu_rel_sub</span></a></span></h2>
+<a id="lab18"></a><h3 class="section">Lemmas about <span class="inlinecode"><a class="idref" href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html#glu_rel_sub"><span class="id" title="definition">glu_rel_sub</span></a></span></h3>
 
 </div>
 <div class="code">
diff --git a/Mcltt.Core.Syntactic.Syntax.html b/Mcltt.Core.Syntactic.Syntax.html
index bc28a03..faf445e 100644
--- a/Mcltt.Core.Syntactic.Syntax.html
+++ b/Mcltt.Core.Syntactic.Syntax.html
@@ -37,7 +37,7 @@ <h1 class="libtitle">Mcltt.Core.Syntactic.Syntax</h1>
 </div>
 
 <div class="doc">
-<a id="lab16"></a><h2 class="section">Concrete Syntax Tree</h2>
+<a id="lab19"></a><h1 class="section">Concrete Syntax Tree</h1>
 
 </div>
 <div class="code">
@@ -58,7 +58,7 @@ <h1 class="libtitle">Mcltt.Core.Syntactic.Syntax</h1>
 </div>
 
 <div class="doc">
-<a id="lab17"></a><h2 class="section">Abstract Syntac Tree</h2>
+<a id="lab20"></a><h1 class="section">Abstract Syntac Tree</h1>
 
 </div>
 <div class="code">
@@ -142,7 +142,7 @@ <h1 class="libtitle">Mcltt.Core.Syntactic.Syntax</h1>
 </div>
 
 <div class="doc">
-<a id="lab18"></a><h3 class="section">Syntactic Normal/Neutral Form</h3>
+<a id="lab21"></a><h2 class="section">Syntactic Normal/Neutral Form</h2>
 
 </div>
 <div class="code">
@@ -209,6 +209,13 @@ <h1 class="libtitle">Mcltt.Core.Syntactic.Syntax</h1>
 <span class="id" title="keyword">Open</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">mcltt_scope</span>.<br/>
 
 <br/>
+</div>
+
+<div class="doc">
+<a id="lab22"></a><h2 class="section">Syntactic Notations</h2>
+
+</div>
+<div class="code">
 <span class="id" title="keyword">Module</span> <a id="Syntax_Notations" class="idref" href="#Syntax_Notations"><span class="id" title="module">Syntax_Notations</span></a>.<br/>
 &nbsp;&nbsp;<span class="id" title="keyword">Notation</span> <a id="ff90a81e6f1b3c561f471442d9455cb9" class="idref" href="#ff90a81e6f1b3c561f471442d9455cb9"><span class="id" title="notation">&quot;</span></a>{{{ x }}}" := <span class="id" title="var">x</span> (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">x</span> <span class="id" title="var">custom</span> <span class="id" title="var">exp</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 99, <span class="id" title="var">format</span> "'{{{'  x  '}}}'") : <span class="id" title="var">mcltt_scope</span>.<br/>
 &nbsp;&nbsp;<span class="id" title="keyword">Notation</span> <a id="b8b673de4d770a3cbcbccee376638293" class="idref" href="#b8b673de4d770a3cbcbccee376638293"><span class="id" title="notation">&quot;</span></a>( x )" := <span class="id" title="var">x</span> (<span class="id" title="tactic">in</span> <span class="id" title="var">custom</span> <span class="id" title="var">exp</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">x</span> <span class="id" title="var">custom</span> <span class="id" title="var">exp</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60) : <span class="id" title="var">mcltt_scope</span>.<br/>
diff --git a/Mcltt.Core.Syntactic.System.Lemmas.html b/Mcltt.Core.Syntactic.System.Lemmas.html
index 83da288..f0fcc88 100644
--- a/Mcltt.Core.Syntactic.System.Lemmas.html
+++ b/Mcltt.Core.Syntactic.System.Lemmas.html
@@ -35,7 +35,7 @@ <h1 class="libtitle">Mcltt.Core.Syntactic.System.Lemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab19"></a><h2 class="section">Core Presuppositions</h2>
+<a id="lab23"></a><h3 class="section">Core Presuppositions</h3>
 
 </div>
 <div class="code">
@@ -318,7 +318,7 @@ <h1 class="libtitle">Mcltt.Core.Syntactic.System.Lemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab20"></a><h2 class="section">Additional Lemmas for Syntactic PERs</h2>
+<a id="lab24"></a><h3 class="section">Additional Lemmas for Syntactic PERs</h3>
 
 </div>
 <div class="code">
@@ -362,7 +362,7 @@ <h1 class="libtitle">Mcltt.Core.Syntactic.System.Lemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab21"></a><h2 class="section">Lemmas for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#exp"><span class="id" title="inductive">exp</span></a></span> of <span class="inlinecode">{{{</span> <span class="inlinecode"><span class="id" title="var">Type@i</span></span> <span class="inlinecode">}}}</span></h2>
+<a id="lab25"></a><h3 class="section">Lemmas for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#exp"><span class="id" title="inductive">exp</span></a></span> of <span class="inlinecode">{{{</span> <span class="inlinecode"><span class="id" title="var">Type@i</span></span> <span class="inlinecode">}}}</span></h3>
 
 </div>
 <div class="code">
@@ -621,7 +621,7 @@ <h1 class="libtitle">Mcltt.Core.Syntactic.System.Lemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab22"></a><h2 class="section">Lemmas for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#exp"><span class="id" title="inductive">exp</span></a></span> of <span class="inlinecode">{{{</span> <span class="inlinecode"><span class="id" title="var">ℕ</span></span> <span class="inlinecode">}}}</span></h2>
+<a id="lab26"></a><h3 class="section">Lemmas for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Syntactic.Syntax.html#exp"><span class="id" title="inductive">exp</span></a></span> of <span class="inlinecode">{{{</span> <span class="inlinecode"><span class="id" title="var">ℕ</span></span> <span class="inlinecode">}}}</span></h3>
 
 </div>
 <div class="code">
@@ -854,7 +854,7 @@ <h1 class="libtitle">Mcltt.Core.Syntactic.System.Lemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab23"></a><h2 class="section">Other Tedious Lemmas</h2>
+<a id="lab27"></a><h3 class="section">Other Tedious Lemmas</h3>
 
 </div>
 <div class="code">
@@ -1240,7 +1240,7 @@ <h1 class="libtitle">Mcltt.Core.Syntactic.System.Lemmas</h1>
 </div>
 
 <div class="doc">
-<a id="lab24"></a><h2 class="section">Lemmas for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#wf_subtyp"><span class="id" title="inductive">wf_subtyp</span></a></span></h2>
+<a id="lab28"></a><h3 class="section">Lemmas for <span class="inlinecode"><a class="idref" href="Mcltt.Core.Syntactic.System.Definitions.html#wf_subtyp"><span class="id" title="inductive">wf_subtyp</span></a></span></h3>
 
 </div>
 <div class="code">
diff --git a/Mcltt.Frontend.Elaborator.html b/Mcltt.Frontend.Elaborator.html
index 8ecf2c4..6fc47b9 100644
--- a/Mcltt.Frontend.Elaborator.html
+++ b/Mcltt.Frontend.Elaborator.html
@@ -282,7 +282,7 @@ <h1 class="libtitle">Mcltt.Frontend.Elaborator</h1>
 </div>
 
 <div class="doc">
-<a id="lab25"></a><h2 class="section">Well scopedness lemma</h2>
+<a id="lab29"></a><h3 class="section">Well scopedness lemma</h3>
 
 <div class="paragraph"> </div>
 
diff --git a/Mcltt.LibTactics.html b/Mcltt.LibTactics.html
index 80fa086..ec68c79 100644
--- a/Mcltt.LibTactics.html
+++ b/Mcltt.LibTactics.html
@@ -51,7 +51,7 @@ <h1 class="libtitle">Mcltt.LibTactics</h1>
 </div>
 
 <div class="doc">
-<a id="lab26"></a><h2 class="section">Generalization of Variables</h2>
+<a id="lab30"></a><h3 class="section">Generalization of Variables</h3>
 
 </div>
 <div class="code">
@@ -66,7 +66,7 @@ <h1 class="libtitle">Mcltt.LibTactics</h1>
 </div>
 
 <div class="doc">
-<a id="lab27"></a><h2 class="section">Marking-based Tactics</h2>
+<a id="lab31"></a><h3 class="section">Marking-based Tactics</h3>
 
 </div>
 <div class="code">
@@ -121,7 +121,7 @@ <h1 class="libtitle">Mcltt.LibTactics</h1>
 </div>
 
 <div class="doc">
-<a id="lab28"></a><h2 class="section">Simple helper</h2>
+<a id="lab32"></a><h3 class="section">Simple helper</h3>
 
 </div>
 <div class="code">
@@ -281,7 +281,7 @@ <h1 class="libtitle">Mcltt.LibTactics</h1>
 </div>
 
 <div class="doc">
-<a id="lab29"></a><h2 class="section">McLTT automation</h2>
+<a id="lab33"></a><h3 class="section">McLTT automation</h3>
 
 </div>
 <div class="code">
@@ -555,7 +555,7 @@ <h1 class="libtitle">Mcltt.LibTactics</h1>
 </div>
 
 <div class="doc">
-<a id="lab30"></a><h2 class="section">Helper Instances for Generalized Rewriting</h2>
+<a id="lab34"></a><h3 class="section">Helper Instances for Generalized Rewriting</h3>
 
 </div>
 <div class="code">
diff --git a/toc.html b/toc.html
index 01dfcf0..8c2c93e 100644
--- a/toc.html
+++ b/toc.html
@@ -59,23 +59,24 @@ <h2><a href="Mcltt.Core.Semantic.PER.html">Mcltt.Core.Semantic.PER</a></h2>
 <h2><a href="Mcltt.Core.Semantic.PER.CoreTactics.html">Mcltt.Core.Semantic.PER.CoreTactics</a></h2>
 <h2><a href="Mcltt.Core.Semantic.PER.Definitions.html">Mcltt.Core.Semantic.PER.Definitions</a></h2>
 <ul class="doclist">
-<li><ul class="doclist">
-<li><a href="Mcltt.Core.Semantic.PER.Definitions.html#lab1">Helper Bundles</a>
+<li><a href="Mcltt.Core.Semantic.PER.Definitions.html#lab3">Universe/Element PER</a>
+<ul class="doclist">
+<li><a href="Mcltt.Core.Semantic.PER.Definitions.html#lab4">Universe/Element PER Definition</a>
 
 </li>
-<li><a href="Mcltt.Core.Semantic.PER.Definitions.html#lab2">(Some Elements of) PER Lattice</a>
+<li><a href="Mcltt.Core.Semantic.PER.Definitions.html#lab5">Universe/Element PER Induction Principle</a>
 
 </li>
-<li><a href="Mcltt.Core.Semantic.PER.Definitions.html#lab3">Universe/Element PER Definition</a>
+</ul>
 
 </li>
-<li><a href="Mcltt.Core.Semantic.PER.Definitions.html#lab4">Universe/Element PER Induction Principle</a>
+<li><a href="Mcltt.Core.Semantic.PER.Definitions.html#lab6">Universe Subtyping</a>
 
 </li>
-<li><a href="Mcltt.Core.Semantic.PER.Definitions.html#lab5">Context/Environment PER</a>
+<li><a href="Mcltt.Core.Semantic.PER.Definitions.html#lab7">Context/Environment PER</a>
 
 </li>
-</ul>
+<li><a href="Mcltt.Core.Semantic.PER.Definitions.html#lab8">Context Subtyping</a>
 
 </li>
 </ul>
@@ -91,51 +92,9 @@ <h2><a href="Mcltt.Core.Soundness.FundamentalTheorem.html">Mcltt.Core.Soundness.
 <h2><a href="Mcltt.Core.Soundness.LogicalRelation.html">Mcltt.Core.Soundness.LogicalRelation</a></h2>
 <h2><a href="Mcltt.Core.Soundness.LogicalRelation.Core.html">Mcltt.Core.Soundness.LogicalRelation.Core</a></h2>
 <h2><a href="Mcltt.Core.Soundness.LogicalRelation.CoreLemmas.html">Mcltt.Core.Soundness.LogicalRelation.CoreLemmas</a></h2>
-<ul class="doclist">
-<li><ul class="doclist">
-<li><a href="Mcltt.Core.Soundness.LogicalRelation.CoreLemmas.html#lab6">Simple Morphism instance for <span class="inlinecode"><span class="id" title="var">glu_univ_elem</span></span></a>
-
-</li>
-<li><a href="Mcltt.Core.Soundness.LogicalRelation.CoreLemmas.html#lab7">Morphism instances for <span class="inlinecode"><span class="id" title="var">neut_glu_</span>*<span class="id" title="var">_pred</span></span>s</a>
-
-</li>
-<li><a href="Mcltt.Core.Soundness.LogicalRelation.CoreLemmas.html#lab8">Morphism instances for <span class="inlinecode"><span class="id" title="var">pi_glu_</span>*<span class="id" title="var">_pred</span></span>s</a>
-
-</li>
-<li><a href="Mcltt.Core.Soundness.LogicalRelation.CoreLemmas.html#lab9">Morphism instances for <span class="inlinecode"><span class="id" title="var">glu_univ_elem</span></span></a>
-
-</li>
-<li><a href="Mcltt.Core.Soundness.LogicalRelation.CoreLemmas.html#lab10">Simple Morphism instance for <span class="inlinecode"><span class="id" title="var">glu_ctx_env</span></span></a>
-
-</li>
-</ul>
-
-</li>
-</ul>
 <h2><a href="Mcltt.Core.Soundness.LogicalRelation.CoreTactics.html">Mcltt.Core.Soundness.LogicalRelation.CoreTactics</a></h2>
 <h2><a href="Mcltt.Core.Soundness.LogicalRelation.Definitions.html">Mcltt.Core.Soundness.LogicalRelation.Definitions</a></h2>
 <h2><a href="Mcltt.Core.Soundness.LogicalRelation.Lemmas.html">Mcltt.Core.Soundness.LogicalRelation.Lemmas</a></h2>
-<ul class="doclist">
-<li><ul class="doclist">
-<li><a href="Mcltt.Core.Soundness.LogicalRelation.Lemmas.html#lab11">Lemmas for <span class="inlinecode"><span class="id" title="var">glu_rel_typ_with_sub</span></span> and <span class="inlinecode"><span class="id" title="var">glu_rel_exp_with_sub</span></span></a>
-
-</li>
-<li><a href="Mcltt.Core.Soundness.LogicalRelation.Lemmas.html#lab12">Lemmas for <span class="inlinecode"><span class="id" title="var">glu_ctx_env</span></span></a>
-
-</li>
-<li><a href="Mcltt.Core.Soundness.LogicalRelation.Lemmas.html#lab13">Tactics for <span class="inlinecode"><span class="id" title="var">glu_rel_</span>*</span></a>
-
-</li>
-<li><a href="Mcltt.Core.Soundness.LogicalRelation.Lemmas.html#lab14">Lemmas about <span class="inlinecode"><span class="id" title="var">glu_rel_exp</span></span></a>
-
-</li>
-<li><a href="Mcltt.Core.Soundness.LogicalRelation.Lemmas.html#lab15">Lemmas about <span class="inlinecode"><span class="id" title="var">glu_rel_sub</span></span></a>
-
-</li>
-</ul>
-
-</li>
-</ul>
 <h2><a href="Mcltt.Core.Soundness.NatCases.html">Mcltt.Core.Soundness.NatCases</a></h2>
 <h2><a href="Mcltt.Core.Soundness.Realizability.html">Mcltt.Core.Soundness.Realizability</a></h2>
 <h2><a href="Mcltt.Core.Soundness.SubstitutionCases.html">Mcltt.Core.Soundness.SubstitutionCases</a></h2>
@@ -154,44 +113,24 @@ <h2><a href="Mcltt.Core.Syntactic.ExpNoConfusion.html">Mcltt.Core.Syntactic.ExpN
 <h2><a href="Mcltt.Core.Syntactic.Presup.html">Mcltt.Core.Syntactic.Presup</a></h2>
 <h2><a href="Mcltt.Core.Syntactic.Syntax.html">Mcltt.Core.Syntactic.Syntax</a></h2>
 <ul class="doclist">
-<li><ul class="doclist">
-<li><a href="Mcltt.Core.Syntactic.Syntax.html#lab16">Concrete Syntax Tree</a>
-
-</li>
-<li><a href="Mcltt.Core.Syntactic.Syntax.html#lab17">Abstract Syntac Tree</a>
-
-</li>
-</ul>
+<li><a href="Mcltt.Core.Syntactic.Syntax.html#lab19">Concrete Syntax Tree</a>
 
 </li>
-</ul>
-<h2><a href="Mcltt.Core.Syntactic.System.html">Mcltt.Core.Syntactic.System</a></h2>
-<h2><a href="Mcltt.Core.Syntactic.System.Definitions.html">Mcltt.Core.Syntactic.System.Definitions</a></h2>
-<h2><a href="Mcltt.Core.Syntactic.System.Lemmas.html">Mcltt.Core.Syntactic.System.Lemmas</a></h2>
+<li><a href="Mcltt.Core.Syntactic.Syntax.html#lab20">Abstract Syntac Tree</a>
 <ul class="doclist">
-<li><ul class="doclist">
-<li><a href="Mcltt.Core.Syntactic.System.Lemmas.html#lab19">Core Presuppositions</a>
-
-</li>
-<li><a href="Mcltt.Core.Syntactic.System.Lemmas.html#lab20">Additional Lemmas for Syntactic PERs</a>
-
-</li>
-<li><a href="Mcltt.Core.Syntactic.System.Lemmas.html#lab21">Lemmas for <span class="inlinecode"><span class="id" title="var">exp</span></span> of <span class="inlinecode">{{{</span> <span class="inlinecode"><span class="id" title="var">Type@i</span></span> <span class="inlinecode">}}}</span></a>
-
-</li>
-<li><a href="Mcltt.Core.Syntactic.System.Lemmas.html#lab22">Lemmas for <span class="inlinecode"><span class="id" title="var">exp</span></span> of <span class="inlinecode">{{{</span> <span class="inlinecode"><span class="id" title="var">ℕ</span></span> <span class="inlinecode">}}}</span></a>
+<li><a href="Mcltt.Core.Syntactic.Syntax.html#lab21">Syntactic Normal/Neutral Form</a>
 
 </li>
-<li><a href="Mcltt.Core.Syntactic.System.Lemmas.html#lab23">Other Tedious Lemmas</a>
-
-</li>
-<li><a href="Mcltt.Core.Syntactic.System.Lemmas.html#lab24">Lemmas for <span class="inlinecode"><span class="id" title="var">wf_subtyp</span></span></a>
+<li><a href="Mcltt.Core.Syntactic.Syntax.html#lab22">Syntactic Notations</a>
 
 </li>
 </ul>
 
 </li>
 </ul>
+<h2><a href="Mcltt.Core.Syntactic.System.html">Mcltt.Core.Syntactic.System</a></h2>
+<h2><a href="Mcltt.Core.Syntactic.System.Definitions.html">Mcltt.Core.Syntactic.System.Definitions</a></h2>
+<h2><a href="Mcltt.Core.Syntactic.System.Lemmas.html">Mcltt.Core.Syntactic.System.Lemmas</a></h2>
 <h2><a href="Mcltt.Core.Syntactic.System.Tactics.html">Mcltt.Core.Syntactic.System.Tactics</a></h2>
 <h2><a href="Mcltt.Core.Syntactic.SystemOpt.html">Mcltt.Core.Syntactic.SystemOpt</a></h2>
 <h2><a href="Mcltt.Entrypoint.html">Mcltt.Entrypoint</a></h2>
@@ -202,38 +141,8 @@ <h2><a href="Mcltt.Extraction.Readback.html">Mcltt.Extraction.Readback</a></h2>
 <h2><a href="Mcltt.Extraction.Subtyping.html">Mcltt.Extraction.Subtyping</a></h2>
 <h2><a href="Mcltt.Extraction.TypeCheck.html">Mcltt.Extraction.TypeCheck</a></h2>
 <h2><a href="Mcltt.Frontend.Elaborator.html">Mcltt.Frontend.Elaborator</a></h2>
-<ul class="doclist">
-<li><ul class="doclist">
-<li><a href="Mcltt.Frontend.Elaborator.html#lab25">Well scopedness lemma</a>
-
-</li>
-</ul>
-
-</li>
-</ul>
 <h2><a href="Mcltt.Frontend.Parser.html">Mcltt.Frontend.Parser</a></h2>
 <h2><a href="Mcltt.LibTactics.html">Mcltt.LibTactics</a></h2>
-<ul class="doclist">
-<li><ul class="doclist">
-<li><a href="Mcltt.LibTactics.html#lab26">Generalization of Variables</a>
-
-</li>
-<li><a href="Mcltt.LibTactics.html#lab27">Marking-based Tactics</a>
-
-</li>
-<li><a href="Mcltt.LibTactics.html#lab28">Simple helper</a>
-
-</li>
-<li><a href="Mcltt.LibTactics.html#lab29">McLTT automation</a>
-
-</li>
-<li><a href="Mcltt.LibTactics.html#lab30">Helper Instances for Generalized Rewriting</a>
-
-</li>
-</ul>
-
-</li>
-</ul>
 </div>
 </div>
 <div id="footer">