From 54248a2e7ff4883184386f898d11ebe3fde69a62 Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Fri, 15 Dec 2023 03:23:06 -0500
Subject: [PATCH] Update syntax

---
 theories/CtxEqLemmas.v  |  32 +--
 theories/CtxEquiv.v     |  23 +-
 theories/Presup.v       |  36 ++--
 theories/PresupLemmas.v |  12 +-
 theories/Relations.v    |  10 +-
 theories/Syntax.v       |  49 ++---
 theories/System.v       | 465 +++++++++++++++++++---------------------
 7 files changed, 301 insertions(+), 326 deletions(-)

diff --git a/theories/CtxEqLemmas.v b/theories/CtxEqLemmas.v
index 922109f5..99c2ba20 100644
--- a/theories/CtxEqLemmas.v
+++ b/theories/CtxEqLemmas.v
@@ -3,26 +3,26 @@ Require Import Mcltt.Syntax.
 Require Export Mcltt.System.
 Require Export Mcltt.LibTactics.
 
-Lemma ctx_decomp : forall {Γ T}, ⊢ T :: Γ -> (⊢ Γ ∧ ∃ i, Γ ⊢ T : typ i).
+Lemma ctx_decomp : forall {Γ T}, {{ ⊢ Γ , T }} -> {{ ⊢ Γ }} ∧ ∃ i, {{ Γ ⊢ T : Type@i }}.
 Proof with mauto.
   intros * HTΓ.
   inversion HTΓ; subst...
 Qed.
 
 (* Corresponds to presup-⊢≈ in the Agda proof *)
-Lemma presup_ctx_eq : forall {Γ Δ}, ⊢ Γ ≈ Δ -> ⊢ Γ ∧ ⊢ Δ.
+Lemma presup_ctx_eq : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Γ }} ∧ {{ ⊢ Δ }}.
 Proof with mauto.
   intros * HΓΔ.
   induction HΓΔ as [|* ? [? ?]]...
 Qed.
 
-(* Corresponds to ≈-refl in the Agda code*)
-Lemma tm_eq_refl : forall {Γ t T}, Γ ⊢ t : T -> Γ ⊢ t ≈ t : T.
+(* Corresponds to ≈-refl in the Agda code *)
+Lemma tm_eq_refl : forall {Γ t T}, {{ Γ ⊢ t : T }} -> {{ Γ ⊢ t ≈ t : T }}.
 Proof.
   mauto.
 Qed.
 
-Lemma sb_eq_refl : forall {Γ Δ σ}, Γ ⊢s σ : Δ -> Γ ⊢s σ ≈ σ : Δ.
+Lemma sb_eq_refl : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢s σ ≈ σ : Δ }}.
 Proof.
   mauto.
 Qed.
@@ -31,22 +31,22 @@ Qed.
 Hint Resolve ctx_decomp presup_ctx_eq tm_eq_refl sb_eq_refl : mcltt.
 
 (* Corresponds to t[σ]-Se in the Agda proof *)
-Lemma sub_lvl : forall {Δ Γ T σ i}, Δ ⊢ T : typ i -> Γ ⊢s σ : Δ -> Γ ⊢ a_sub T σ : typ i.
+Lemma exp_sub_typ : forall {Δ Γ T σ i}, {{ Δ ⊢ T : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ T[σ] : Type@i }}.
 Proof.
   mauto.
 Qed.
 
 (* Corresponds to []-cong-Se′ in the Agda proof*)
-Lemma sub_lvl_eq : forall {Δ Γ T T' σ i}, Δ ⊢ T ≈ T' : typ i -> Γ ⊢s σ : Δ -> Γ ⊢ a_sub T σ ≈ a_sub T' σ : typ i.
+Lemma eq_exp_sub_typ : forall {Δ Γ T T' σ i}, {{ Δ ⊢ T ≈ T' : Type@i }} -> {{ Γ ⊢s σ : Δ }} -> {{ Γ ⊢ T[σ] ≈ T'[σ] : Type@i }}.
 Proof.
   mauto.
 Qed.
 
 #[export]
-Hint Resolve sub_lvl sub_lvl_eq : mcltt.
+Hint Resolve exp_sub_typ eq_exp_sub_typ : mcltt.
 
 (* Corresponds to ∈!⇒ty-wf in Agda proof *)
-Lemma var_in_wf : forall {Γ T x}, ⊢ Γ -> x : T ∈! Γ -> ∃ i, Γ ⊢ T : typ i.
+Lemma var_in_wf : forall {Γ T x}, {{ ⊢ Γ }} -> {{ #x : T ∈ Γ }} -> ∃ i, {{ Γ ⊢ T : Type@i }}.
 Proof with mauto.
   intros * HΓ Hx. gen x T.
   induction HΓ; intros; inversion_clear Hx as [|? ? ? ? Hx']...
@@ -56,7 +56,7 @@ Qed.
 #[export]
 Hint Resolve var_in_wf : mcltt.
 
-Lemma presup_sb_ctx : forall {Γ Δ σ}, Γ ⊢s σ : Δ -> ⊢ Γ ∧ ⊢ Δ.
+Lemma presup_sb_ctx : forall {Γ Δ σ}, {{ Γ ⊢s σ : Δ }} -> {{ ⊢ Γ }} ∧ {{ ⊢ Δ }}.
 Proof with mauto.
   intros * Hσ.
   induction Hσ...
@@ -70,7 +70,7 @@ Qed.
 #[export]
 Hint Resolve presup_sb_ctx : mcltt.
 
-Lemma presup_tm_ctx : forall {Γ t T}, Γ ⊢ t : T -> ⊢ Γ.
+Lemma presup_tm_ctx : forall {Γ t T}, {{ Γ ⊢ t : T }} -> {{ ⊢ Γ }}.
 Proof with mauto.
   intros * Ht.
   induction Ht...
@@ -81,7 +81,7 @@ Qed.
 Hint Resolve presup_tm_ctx : mcltt.
 
 (* Corresponds to ∈!⇒ty≈ in Agda proof *)
-Lemma var_in_eq : forall {Γ Δ T x}, ⊢ Γ ≈ Δ -> x : T ∈! Γ -> ∃ S i, x : S ∈! Δ ∧ Γ ⊢ T ≈ S : typ i ∧ Δ ⊢ T ≈ S : typ i.
+Lemma var_in_eq : forall {Γ Δ T x}, {{ ⊢ Γ ≈ Δ }} -> {{ #x : T ∈ Γ }} -> ∃ S i, {{ #x : S ∈ Δ }} ∧ {{ Γ ⊢ T ≈ S : Type@i }} ∧ {{ Δ ⊢ T ≈ S : Type@i }}.
 Proof with mauto.
   intros * HΓΔ Hx.
   gen Δ; induction Hx; intros; inversion_clear HΓΔ as [|? ? ? ? ? HΓΔ'].
@@ -91,7 +91,7 @@ Proof with mauto.
 Qed.
 
 (* Corresponds to ⊢≈-sym in Agda proof *)
-Lemma ctx_eq_sym : forall {Γ Δ}, ⊢ Γ ≈ Δ -> ⊢ Δ ≈ Γ.
+Lemma ctx_eq_sym : forall {Γ Δ}, {{ ⊢ Γ ≈ Δ }} -> {{ ⊢ Δ ≈ Γ }}.
 Proof with mauto.
   intros.
   induction H...
@@ -100,7 +100,7 @@ Qed.
 #[export]
 Hint Resolve var_in_eq ctx_eq_sym : mcltt.
 
-Lemma presup_sb_eq_ctx : forall {Γ Δ σ σ'}, Γ ⊢s σ ≈ σ' : Δ -> ⊢ Γ.
+Lemma presup_sb_eq_ctx : forall {Γ Δ σ σ'}, {{ Γ ⊢s σ ≈ σ' : Δ }} -> {{ ⊢ Γ }}.
 Proof with mauto.
   intros.
   induction H; mauto; now (eapply proj1; mauto).
@@ -109,12 +109,12 @@ Qed.
 #[export]
 Hint Resolve presup_sb_eq_ctx : mcltt.
 
-Lemma presup_tm_eq_ctx : forall {Γ t t' T}, Γ ⊢ t ≈ t' : T -> ⊢ Γ.
+Lemma presup_tm_eq_ctx : forall {Γ t t' T}, {{ Γ ⊢ t ≈ t' : T }} -> {{ ⊢ Γ }}.
 Proof with mauto.
   intros.
   induction H...
   Unshelve.
-  exact 0%nat.
+  constructor.
 Qed.
 
 #[export]
diff --git a/theories/CtxEquiv.v b/theories/CtxEquiv.v
index 5f902964..55d1d9c1 100644
--- a/theories/CtxEquiv.v
+++ b/theories/CtxEquiv.v
@@ -4,31 +4,26 @@ Require Import Mcltt.System.
 Require Import Mcltt.CtxEqLemmas.
 Require Import Mcltt.LibTactics.
 
-Lemma ctxeq_tm : forall {Γ Δ t T}, ⊢ Γ ≈ Δ -> Γ ⊢ t : T -> Δ ⊢ t : T
+Lemma ctxeq_tm : forall {Γ Δ t T}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ t : T }} -> {{ Δ ⊢ t : T }}
 with
-ctxeq_eq : forall {Γ Δ t t' T}, ⊢ Γ ≈ Δ -> Γ ⊢ t ≈ t' : T -> Δ ⊢ t ≈ t' : T
+ctxeq_eq : forall {Γ Δ t t' T}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢ t ≈ t' : T }} -> {{ Δ ⊢ t ≈ t' : T }}
 with
-ctxeq_s : forall {Γ Γ' Δ σ}, ⊢ Γ ≈ Δ -> Γ ⊢s σ : Γ' -> Δ ⊢s σ : Γ'
+ctxeq_s : forall {Γ Γ' Δ σ}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢s σ : Γ' }} -> {{ Δ ⊢s σ : Γ' }}
 with
-ctxeq_s_eq : forall {Γ Γ' Δ σ σ'}, ⊢ Γ ≈ Δ -> Γ ⊢s σ ≈ σ' : Γ' -> Δ ⊢s σ ≈ σ' : Γ'.
+ctxeq_s_eq : forall {Γ Γ' Δ σ σ'}, {{ ⊢ Γ ≈ Δ }} -> {{ Γ ⊢s σ ≈ σ' : Γ' }} -> {{ Δ ⊢s σ ≈ σ' : Γ' }}.
 Proof with mauto.
   (*ctxeq_tm*)
   - clear ctxeq_tm.
     intros * HΓΔ Ht.
     gen Δ.
     induction Ht; intros; destruct (presup_ctx_eq HΓΔ)...
-    -- destruct (presup_ctx_eq HΓΔ) as [G D].
-       pose proof (IHHt1 _ HΓΔ).
-       assert (⊢ a :: Γ ≈ a :: Δ)...
-    -- destruct (presup_ctx_eq HΓΔ) as [G D].
-       pose proof (IHHt1 _ HΓΔ).
-       assert (⊢ A :: Γ ≈ A :: Δ)...
+    -- pose proof (IHHt1 _ HΓΔ).
+       assert ({{ ⊢ Γ , A ≈ Δ , A }})...
     -- destruct (var_in_eq HΓΔ H0) as [T' [i [xT'G [GTT' DTT']]]].
        eapply wf_conv...
-    -- destruct (presup_ctx_eq HΓΔ) as [G D].
-       assert (⊢ A :: Γ ≈ A :: Δ); mauto 6.
+    -- assert ({{ ⊢ Γ , A ≈ Δ , A }}); mauto 6.
     -- pose proof (IHHt1 _ HΓΔ).
-       assert (⊢ A :: Γ ≈ A :: Δ)...
+       assert ({{ ⊢ Γ , A ≈ Δ , A }})...
   (*ctxeq_eq*)
   - clear ctxeq_eq.
     intros * HΓΔ Htt'.
@@ -37,7 +32,7 @@ Proof with mauto.
     1-4,6-19: mauto.
     -- pose proof (IHHtt'1 _ HΓΔ).
        pose proof (ctxeq_tm _ _ _ _ HΓΔ H).
-       assert (⊢ M :: Γ ≈ M :: Δ)...
+       assert ({{ ⊢ Γ , M ≈ Δ , M }})...
     -- inversion_clear HΓΔ.
        pose proof (var_in_eq H3 H0) as [T'' [n [xT'' [GTT'' DTT'']]]].
        destruct (presup_ctx_eq H3).
diff --git a/theories/Presup.v b/theories/Presup.v
index ac56d223..4dfa789b 100644
--- a/theories/Presup.v
+++ b/theories/Presup.v
@@ -19,11 +19,11 @@ Ltac breakdown_goal :=
 
 Ltac gen_presup_ctx H :=
   match type of H with
-  | ⊢ ?Γ ≈ ?Δ =>
+  | {{ ⊢ ?Γ ≈ ?Δ }} =>
       let HΓ := fresh "HΓ" in
       let HΔ := fresh "HΔ" in
       pose proof presup_ctx_eq H as [HΓ HΔ]
-  | ?Γ ⊢s ?σ : ?Δ =>
+  | {{ ?Γ ⊢s ?σ : ?Δ }} =>
       let HΓ := fresh "HΓ" in
       let HΔ := fresh "HΔ" in
       pose proof presup_sb_ctx H as [HΓ HΔ]
@@ -32,18 +32,18 @@ Ltac gen_presup_ctx H :=
 
 Ltac gen_presup_IH presup_tm presup_eq presup_sb_eq H :=
   match type of H with
-  | (?Γ ⊢ ?t : ?T) =>
+  | {{ ?Γ ⊢ ?t : ?T }} =>
       let HΓ := fresh "HΓ" in
       let i := fresh "i" in
       let HTi := fresh "HTi" in
       pose proof presup_tm _ _ _ H as [HΓ [i HTi]]
-  | ?Γ ⊢s ?σ ≈ ?τ : ?Δ =>
+  | {{ ?Γ ⊢s ?σ ≈ ?τ : ?Δ }} =>
       let HΓ := fresh "HΓ" in
       let Hσ := fresh "Hσ" in
       let Hτ := fresh "Hτ" in
       let HΔ := fresh "HΔ" in
       pose proof presup_sb_eq _ _ _ _ H as [HΓ [Hσ [Hτ HΔ]]]
-  | ?Γ ⊢ ?s ≈ ?t : ?T =>
+  | {{ ?Γ ⊢ ?s ≈ ?t : ?T }} =>
       let HΓ := fresh "HΓ" in
       let i := fresh "i" in
       let Hs := fresh "Hs" in
@@ -53,14 +53,14 @@ Ltac gen_presup_IH presup_tm presup_eq presup_sb_eq H :=
   | _ => gen_presup_ctx H
   end.
 
-Lemma presup_tm : forall {Γ t T}, Γ ⊢ t : T -> ⊢ Γ ∧ ∃ i, Γ ⊢ T : typ i
-with presup_eq : forall {Γ s t T}, Γ ⊢ s ≈ t : T -> ⊢ Γ ∧ Γ ⊢ s : T ∧ Γ ⊢ t : T ∧ ∃ i,Γ ⊢ T : typ i
-with presup_sb_eq : forall {Γ Δ σ τ}, Γ ⊢s σ ≈ τ : Δ -> ⊢ Γ ∧ Γ ⊢s σ : Δ ∧ Γ ⊢s τ : Δ ∧ ⊢ Δ.
+Lemma presup_tm : forall {Γ t T}, {{ Γ ⊢ t : T }} -> {{ ⊢ Γ }} ∧ ∃ i, {{ Γ ⊢ T : Type@i }}
+with presup_eq : forall {Γ s t T}, {{ Γ ⊢ s ≈ t : T }} -> {{ ⊢ Γ }} ∧ {{ Γ ⊢ s : T }} ∧ {{ Γ ⊢ t : T }} ∧ ∃ i, {{ Γ ⊢ T : Type@i }}
+with presup_sb_eq : forall {Γ Δ σ τ}, {{ Γ ⊢s σ ≈ τ : Δ }} -> {{ ⊢ Γ }} ∧ {{ Γ ⊢s σ : Δ }} ∧ {{ Γ ⊢s τ : Δ }} ∧ {{ ⊢ Δ }}.
 Proof with mauto.
   - intros * Ht.
-    inversion_clear Ht; (on_all_hyp: gen_presup_IH presup_tm presup_eq presup_sb_eq); breakdown_goal.
+    inversion_clear Ht; (on_all_hyp: gen_presup_IH presup_tm presup_eq presup_sb_eq); clear presup_tm presup_eq presup_sb_eq; breakdown_goal.
     -- eexists.
-       eapply sub_lvl...
+       eapply exp_sub_typ...
        econstructor...
     -- eexists.
        pose proof (lift_tm_max_left i0 H).
@@ -68,9 +68,9 @@ Proof with mauto.
        econstructor...
 
   - intros * Hst.
-    inversion_clear Hst; (on_all_hyp: gen_presup_IH presup_tm presup_eq presup_sb_eq); breakdown_goal.
+    inversion_clear Hst; (on_all_hyp: gen_presup_IH presup_tm presup_eq presup_sb_eq); clear presup_tm presup_eq presup_sb_eq; breakdown_goal.
     -- econstructor...
-       eapply sub_lvl...
+       eapply exp_sub_typ...
        econstructor...
        eapply wf_conv...
        eapply wf_eq_conv; mauto 6.
@@ -78,7 +78,7 @@ Proof with mauto.
     -- econstructor...
        eapply wf_eq_conv...
 
-    -- eapply wf_sub...
+    -- eapply wf_exp_sub...
        econstructor...
        inversion H...
 
@@ -88,7 +88,7 @@ Proof with mauto.
        eapply wf_eq_trans.
        + eapply wf_eq_sym.
          eapply wf_eq_conv.
-         ++ eapply wf_eq_sub_comp...
+         ++ eapply wf_eq_exp_sub_compose...
          ++ econstructor...
        + do 2 econstructor...
 
@@ -96,12 +96,12 @@ Proof with mauto.
        eapply wf_eq_trans.
        + eapply wf_eq_sym.
          eapply wf_eq_conv.
-         ++ eapply wf_eq_sub_comp...
+         ++ eapply wf_eq_exp_sub_compose...
          ++ econstructor...
        + do 2 econstructor...
 
   - intros * Hστ.
-    inversion_clear Hστ; (on_all_hyp: gen_presup_IH presup_tm presup_eq presup_sb_eq); breakdown_goal.
+    inversion_clear Hστ; (on_all_hyp: gen_presup_IH presup_tm presup_eq presup_sb_eq); clear presup_tm presup_eq presup_sb_eq; breakdown_goal.
     -- inversion_clear H...
 
     -- econstructor...
@@ -116,8 +116,8 @@ Proof with mauto.
        eapply wf_conv...
        eapply wf_eq_conv...
 
-  Unshelve.
-  all: exact 0.
+    Unshelve.
+    all: constructor.
 Qed.
 
 #[export]
diff --git a/theories/PresupLemmas.v b/theories/PresupLemmas.v
index cc534e14..e4555daa 100644
--- a/theories/PresupLemmas.v
+++ b/theories/PresupLemmas.v
@@ -8,7 +8,7 @@ Require Import Setoid.
 
 (*Type lifting lemmas*)
 
-Lemma lift_tm_ge : forall {Γ T n m}, n <= m -> Γ ⊢ T : typ n -> Γ ⊢ T : typ m.
+Lemma lift_tm_ge : forall {Γ T n m}, n <= m -> {{ Γ ⊢ T : Type@n }} -> {{ Γ ⊢ T : Type@m }}.
 Proof with mauto.
   intros * Hnm HT.
   induction m; inversion Hnm; subst...
@@ -17,19 +17,19 @@ Qed.
 #[export]
 Hint Resolve lift_tm_ge : mcltt.
 
-Lemma lift_tm_max_left : forall {Γ T n} m, Γ ⊢ T : typ n -> Γ ⊢ T : typ (max n m).
+Lemma lift_tm_max_left : forall {Γ T n} m, {{ Γ ⊢ T : Type@n }} -> {{ Γ ⊢ T : Type@(max n m) }}.
 Proof with mauto.
   intros.
   assert (n <= max n m) by lia...
 Qed.
 
-Lemma lift_tm_max_right : forall {Γ T} n {m}, Γ ⊢ T : typ m -> Γ ⊢ T : typ (max n m).
+Lemma lift_tm_max_right : forall {Γ T} n {m}, {{ Γ ⊢ T : Type@m }} -> {{ Γ ⊢ T : Type@(max n m) }}.
 Proof with mauto.
   intros.
   assert (m <= max n m) by lia...
 Qed.
 
-Lemma lift_eq_ge : forall {Γ T T' n m}, n <= m -> Γ ⊢ T ≈ T': typ n -> Γ ⊢ T ≈ T' : typ m.
+Lemma lift_eq_ge : forall {Γ T T' n m}, n <= m -> {{ Γ ⊢ T ≈ T': Type@n }} -> {{ Γ ⊢ T ≈ T' : Type@m }}.
 Proof with mauto.
   intros * Hnm HTT'.
   induction m; inversion Hnm; subst...
@@ -38,13 +38,13 @@ Qed.
 #[export]
 Hint Resolve lift_eq_ge : mcltt.
 
-Lemma lift_eq_max_left : forall {Γ T T' n} m, Γ ⊢ T ≈ T' : typ n -> Γ ⊢ T ≈ T' : typ (max n m).
+Lemma lift_eq_max_left : forall {Γ T T' n} m, {{ Γ ⊢ T ≈ T' : Type@n }} -> {{ Γ ⊢ T ≈ T' : Type@(max n m) }}.
 Proof with mauto.
   intros.
   assert (n <= max n m) by lia...
 Qed.
 
-Lemma lift_eq_max_right : forall {Γ T T'} n {m}, Γ ⊢ T ≈ T' : typ m -> Γ ⊢ T ≈ T' : typ (max n m).
+Lemma lift_eq_max_right : forall {Γ T T'} n {m}, {{ Γ ⊢ T ≈ T' : Type@m }} -> {{ Γ ⊢ T ≈ T' : Type@(max n m) }}.
 Proof with mauto.
   intros.
   assert (m <= max n m) by lia...
diff --git a/theories/Relations.v b/theories/Relations.v
index 31dba6c3..bb8f83d1 100644
--- a/theories/Relations.v
+++ b/theories/Relations.v
@@ -8,7 +8,7 @@ Require Import Mcltt.PresupLemmas.
 Require Import Setoid.
 Require Import Coq.Program.Equality.
 
-Lemma ctx_eq_refl : forall {Γ}, ⊢ Γ -> ⊢ Γ ≈ Γ.
+Lemma ctx_eq_refl : forall {Γ}, {{ ⊢ Γ }} -> {{ ⊢ Γ ≈ Γ }}.
 Proof with mauto.
   intros * HΓ.
   induction HΓ...
@@ -17,7 +17,7 @@ Qed.
 #[export]
 Hint Resolve ctx_eq_refl : mcltt.
 
-Lemma ctx_eq_trans : forall {Γ0 Γ1 Γ2}, ⊢ Γ0 ≈ Γ1 -> ⊢ Γ1 ≈ Γ2 -> ⊢ Γ0 ≈ Γ2.
+Lemma ctx_eq_trans : forall {Γ0 Γ1 Γ2}, {{ ⊢ Γ0 ≈ Γ1 }} -> {{ ⊢ Γ1 ≈ Γ2 }} -> {{ ⊢ Γ0 ≈ Γ2 }}.
 Proof with mauto.
   intros * HΓ01 HΓ12.
   gen Γ2.
@@ -31,17 +31,17 @@ Proof with mauto.
   econstructor...
 Qed.
 
-Add Relation (Ctx) (wf_ctx_eq)
+Add Relation (ctx) (wf_ctx_eq)
     symmetry proved by @ctx_eq_sym
     transitivity proved by @ctx_eq_trans
     as ctx_eq.
 
-Add Parametric Relation (Γ : Ctx) (T : Typ) : (exp) (λ t t', Γ ⊢ t ≈ t' : T)
+Add Parametric Relation (Γ : ctx) (T : typ) : (exp) (λ t t', {{ Γ ⊢ t ≈ t' : T }})
     symmetry proved by (λ t t', wf_eq_sym Γ t t' T)
     transitivity proved by (λ t t' t'', wf_eq_trans Γ t t' T t'')
     as tm_eq.                                                
 
-Add Parametric Relation (Γ Δ : Ctx) : (Sb) (λ σ τ, Γ ⊢s σ ≈ τ : Δ)
+Add Parametric Relation (Γ Δ : ctx) : (sub) (λ σ τ, {{ Γ ⊢s σ ≈ τ : Δ }})
     symmetry proved by (λ σ τ, wf_sub_eq_sym Γ σ τ Δ)
     transitivity proved by (λ σ τ ρ, wf_sub_eq_trans Γ σ τ Δ ρ)
     as sb_eq.
diff --git a/theories/Syntax.v b/theories/Syntax.v
index 5e452f45..c814a0ae 100644
--- a/theories/Syntax.v
+++ b/theories/Syntax.v
@@ -28,16 +28,12 @@ Inductive exp : Set :=
   | a_app : exp -> exp -> exp
   | a_pi : exp -> exp -> exp
   (* Substitutions *)
-  | a_sub : exp -> subst -> exp
-with subst : Set :=
-  | a_id : subst
-  | a_weaken : subst
-  | a_compose : subst -> subst -> subst
-  | a_extend : subst -> exp -> subst.
-
-(* Some convenient infix notations *)
-Infix "∙" := a_compose (at level 70).
-Infix ",," := a_extend (at level 80).
+  | a_sub : exp -> sub -> exp
+with sub : Set :=
+  | a_id : sub
+  | a_weaken : sub
+  | a_compose : sub -> sub -> sub
+  | a_extend : sub -> exp -> sub.
 
 Fixpoint nat_to_exp n : exp :=
   match n with
@@ -66,32 +62,33 @@ Definition exp_to_num e :=
 #[global] Declare Scope exp_scope.
 #[global] Delimit Scope exp_scope with exp.
 #[global] Bind Scope exp_scope with exp.
-#[global] Bind Scope exp_scope with subst.
+#[global] Bind Scope exp_scope with sub.
+#[global] Bind Scope exp_scope with Sortclass.
 Open Scope exp_scope.
 Open Scope nat_scope.
 
-Notation "<{ x }>" := x (at level 0, x custom exp at level 99) : exp_scope.
-Notation "( x )" := x (in custom exp at level 0, x custom exp at level 99) : exp_scope.
-Notation "~{ x }" := x (in custom exp at level 0, x constr at level 0) : exp_scope.
+Notation "{{{ x }}}" := x (at level 0, x custom exp at level 99, format "'{{{'  x  '}}}'") : exp_scope.
+Notation "( x )" := x (in custom exp at level 0, x custom exp at level 60) : exp_scope.
+Notation "~ x" := x (in custom exp at level 0, x constr at level 0) : exp_scope.
 Notation "x" := x (in custom exp at level 0, x constr at level 0) : exp_scope.
-Notation "e |[ s ]|" := (a_sub e s) (in custom exp at level 0, s custom exp at level 99) : exp_scope.
+Notation "e [ s ]" := (a_sub e s) (in custom exp at level 0, s custom exp at level 60) : exp_scope.
 Notation "'λ' T e" := (a_fn T e) (in custom exp at level 0, T custom exp at level 30, e custom exp at level 30) : exp_scope.
 Notation "f x .. y" := (a_app .. (a_app f x) .. y) (in custom exp at level 40, f custom exp, x custom exp at next level, y custom exp at next level) : exp_scope.
 Notation "'ℕ'" := a_nat (in custom exp) : exp_scope.
-Notation "'Type(' n ')'" := (a_typ n) (in custom exp at level 0, n constr at level 99) : exp_scope.
+Notation "'Type' @ n" := (a_typ n) (in custom exp at level 0, n constr at level 0) : exp_scope.
 Notation "'Π' T S" := (a_pi T S) (in custom exp at level 0, T custom exp at level 30, S custom exp at level 30) : exp_scope.
 Number Notation exp num_to_exp exp_to_num : exp_scope.
-Notation "'suc' e" := (a_succ e) (in custom exp at level 30, e custom exp at level 30) : exp_scope.
+Notation "'zero'" := a_zero (in custom exp at level 0) : exp_scope.
+Notation "'succ' e" := (a_succ e) (in custom exp at level 30, e custom exp at level 30) : exp_scope.
 Notation "'#' n" := (a_var n) (in custom exp at level 0, n constr at level 0) : exp_scope.
 Notation "'Id'" := a_id (in custom exp at level 0) : exp_scope.
 Notation "'Wk'" := a_weaken (in custom exp at level 0) : exp_scope.
-Infix "∙" := a_compose (in custom exp at level 70) : exp_scope.
-Infix "," := a_extend (in custom exp at level 80) : exp_scope.
 
-Notation Ctx := (list exp).
-Notation Sb := subst.
-Notation Typ := exp.
-Notation typ := a_typ.
-Notation ℕ := a_nat.
-Notation 𝝺 := a_fn.
-Notation Π := a_pi.
+Notation "⋅" := nil (in custom exp at level 0) : exp_scope.
+Notation "x , y" := (cons y x) (in custom exp at level 50) : exp_scope.
+
+Infix "∘" := a_compose (in custom exp at level 40) : exp_scope.
+Infix ",," := a_extend (in custom exp at level 50) : exp_scope.
+
+Notation ctx := (list exp).
+Notation typ := exp.
diff --git a/theories/System.v b/theories/System.v
index 4d02638a..5b098460 100644
--- a/theories/System.v
+++ b/theories/System.v
@@ -5,250 +5,233 @@ Import ListNotations.
 Require Import Mcltt.Syntax.
 Require Import Mcltt.LibTactics.
 
-Reserved Notation "⊢ Γ" (at level 80).
-Reserved Notation "⊢ Γ ≈ Δ" (at level 80, Γ at next level, Δ at next level).
-Reserved Notation "Γ ⊢ A ≈ B : T" (at level 80, A at next level, B at next level).
-Reserved Notation "Γ ⊢ t : T" (no associativity, at level 80, t at next level).
-Reserved Notation "Γ ⊢s σ : Δ" (no associativity, at level 80, σ at next level).
-Reserved Notation "Γ ⊢s S1 ≈ S2 : Δ" (no associativity, at level 80, S1 at next level, S2 at next level).
-Reserved Notation "x : T ∈! Γ" (no associativity, at level 80).
+#[global] Declare Custom Entry judg.
+Notation "{{ x }}" := x (at level 0, x custom judg at level 99, format "'{{'  x  '}}'").
+Reserved Notation "⊢ Γ" (in custom judg at level 80, Γ custom exp).
+Reserved Notation "⊢ Γ ≈ Δ" (in custom judg at level 80, Γ custom exp, Δ custom exp).
+Reserved Notation "Γ ⊢ A ≈ B : T" (in custom judg at level 80, Γ custom exp, A custom exp, B custom exp, T custom exp).
+Reserved Notation "Γ ⊢ t : T" (in custom judg at level 80, Γ custom exp, t custom exp, T custom exp).
+Reserved Notation "Γ ⊢s σ : Δ" (in custom judg at level 80, Γ custom exp, σ custom exp, Δ custom exp).
+Reserved Notation "Γ ⊢s S1 ≈ S2 : Δ" (in custom judg at level 80, Γ custom exp, S1 custom exp, S2 custom exp, Δ custom exp).
+Reserved Notation "'#' x : T ∈ Γ" (in custom judg at level 80, x constr at level 0, T custom exp, Γ custom exp at level 50).
 
 Generalizable All Variables.
 
-Inductive ctx_lookup : nat -> Typ -> Ctx -> Prop :=
-  | here : `( 0 : <{ T|[Wk]| }> ∈! (T :: Γ) )
-  | there : `( n : T ∈! Γ -> (S n) : <{ T|[Wk]| }> ∈! (T' :: Γ) )
-where "x : T ∈! Γ" := (ctx_lookup x T Γ).
-
-
-Inductive wf_ctx : Ctx -> Prop :=
-  | wf_empty : ⊢ []
-  | wf_extend : `(
-      ⊢ Γ ->
-      Γ ⊢ T : typ i ->
-      ⊢ T :: Γ
-    )
-where "⊢ Γ" := (wf_ctx Γ)
-with wf_ctx_eq : Ctx -> Ctx -> Prop :=
-  | wfc_empty : ⊢ [] ≈ []
-  | wfc_extend : `(
-      ⊢ Γ ≈ Δ ->
-      Γ ⊢ T : typ i ->
-      Δ ⊢ T' : typ i ->
-      Γ ⊢ T ≈ T' : (typ i) ->
-      Δ ⊢ T ≈ T' : (typ i) ->
-      ⊢ (T :: Γ) ≈ (T' :: Δ)
-    )
-where "⊢ Γ ≈ Δ" := (wf_ctx_eq Γ Δ)
-with wf_term : Ctx -> exp -> Typ -> Prop :=
-  | wf_univ_nat_f :
-      `(⊢ Γ -> Γ ⊢ ℕ : typ i)
-  | wf_univ :
-      `(⊢ Γ -> Γ ⊢ typ i : typ (i + 1))
-  | wf_univ_fun_f : `(
-      Γ ⊢ a : typ i ->
-      a :: Γ ⊢ b : typ i ->
-      Γ ⊢ 𝝺 a b : typ i
-    )
-  | wf_pi : `(
-      Γ ⊢ A : typ i ->
-      A :: Γ ⊢ B : typ i ->
-      Γ ⊢ Π A B : typ i
-    )
-  | wf_vlookup : `(
-      ⊢ Γ ->
-      x : T ∈! Γ ->
-      Γ ⊢ <{ #x }> : T
-    )
-| wf_fun_e: `(
-      Γ ⊢ A : typ i ->
-      A :: Γ ⊢ B : typ i ->
-      Γ ⊢ M : Π A B ->
-      Γ ⊢ N : A ->
-      Γ ⊢ <{ M N }> : <{ B|[Id,N]| }>
-    )
-  | wf_fun_i : `(
-      Γ ⊢ A : typ i ->
-      A :: Γ ⊢ M : B ->
-      Γ ⊢ 𝝺 A M : Π A B
-    )
-  | wf_zero :
-      `(⊢ Γ -> Γ ⊢ a_zero : ℕ)
-  | wf_succ :
-      `(Γ ⊢ n : ℕ -> Γ ⊢ a_succ n : ℕ)
-  | wf_sub : `(
-      Γ ⊢s σ : Δ ->
-      Δ ⊢ M : A ->
-      Γ ⊢ a_sub M σ : a_sub A σ
-               )
-  | wf_conv : `(
-      Γ ⊢ t : T ->
-      (Γ ⊢ T ≈ T' : (typ i)) ->
-      Γ ⊢ t : T'
-      )
-  | wf_cumu :
-      `(Γ ⊢ T : typ i -> Γ ⊢ T : typ (1 + i))
-where "Γ ⊢ t : T" := (wf_term Γ t T)
-with wf_sb : Ctx -> Sb -> Ctx -> Prop :=
-  | wf_sb_id :
-      `(⊢ Γ -> Γ ⊢s a_id : Γ)
-  | wf_sb_weaken : `(
-      ⊢ A :: Γ ->
-      A :: Γ ⊢s a_weaken : Γ
-    )
-  | wf_sb_compose : `(
-      Γ1 ⊢s σ2 : Γ2 ->
-      Γ2 ⊢s σ1 : Γ3 ->
-      Γ1 ⊢s σ1 ∙ σ2 : Γ3
-    )
-  | wf_sb_extend : `(
-      Γ ⊢s σ : Δ ->
-      Δ ⊢ A : typ i ->
-      Γ ⊢ M : a_sub A σ ->
-      Γ ⊢s (σ ,, M) : A :: Δ
-     )
-  | wf_sb_conv : `(
-      Γ ⊢s σ : Δ ->
-      ⊢ Δ ≈ Δ' ->
-      Γ ⊢s σ : Δ'
-     )
-where "Γ ⊢s σ : Δ" := (wf_sb Γ σ Δ)
-with wf_term_eq : Ctx -> exp -> exp -> Typ -> Prop :=
-  | wf_eq_nat_sub :
-      `(Γ ⊢s σ : Δ -> Γ ⊢ (a_sub ℕ σ) ≈ ℕ : typ i)
-  | wf_eq_typ_sub :
-      `(Γ ⊢s σ : Δ -> Γ ⊢ a_sub (typ i) σ ≈ typ i : typ (i+1))
-  | wf_eq_pi_sub : `(
-      Γ ⊢s σ : Δ ->
-      Δ ⊢ T' : typ i ->
-      T' :: Δ ⊢ T : typ i ->
-      Γ ⊢ a_sub (Π T' T) σ ≈ Π (a_sub T' σ) (a_sub T (σ ∙ a_weaken ,, a_var 0)) : typ i
-    )
-  | wf_eq_pi_cong : `(
-      Γ ⊢ M : typ i ->
-      Γ ⊢ M ≈ M' : typ i ->
-      M :: Γ ⊢ T ≈ T' : typ i ->
-      Γ ⊢ Π M T ≈ Π M' T' : typ i
-    )
-  | wf_eq_var : `(
-      ⊢ Γ ->
-      x : T ∈! Γ ->
-      Γ ⊢ a_var x ≈ a_var x : T
-   )
-  | wf_eq_zero :
-      `(⊢ Γ -> Γ ⊢ a_zero ≈ a_zero : ℕ)
-  | wf_eq_zero_sub :
-      `(Γ ⊢s σ : Δ  -> Γ ⊢ a_sub a_zero σ ≈ a_zero : ℕ)
-  | wf_eq_succ :
-      `(Γ ⊢ t ≈ t' : ℕ -> Γ ⊢ a_succ t ≈ a_succ t' : ℕ)
-  | wf_eq_succ_sub : `(
-      Γ ⊢s σ : Δ ->
-      Δ ⊢ t : ℕ ->
-      Γ ⊢ a_sub (a_succ t) σ ≈ a_succ (a_sub t σ) : ℕ
-    )
-  | wf_eq_sub_cong : `(
-      Δ ⊢ t ≈ t' : T ->
-      Γ ⊢s σ ≈ σ' : Δ ->
-      Γ ⊢ a_sub t σ ≈ a_sub t' σ' : a_sub T σ
-    )
-  | wf_eq_sub_id :
-      `(Γ ⊢ t : T -> Γ ⊢ a_sub t a_id ≈ t : T)
-  | wf_eq_sub_weak : `(
-      ⊢ M :: Γ ->
-      x : T ∈! Γ ->
-      M :: Γ ⊢ a_sub (a_var x) a_weaken ≈ a_var (S x) : a_sub T a_weaken
-   )
-  | wf_eq_sub_comp : `(
-      Γ ⊢s τ : Γ' ->
-      Γ' ⊢s σ : Γ'' ->
-      Γ'' ⊢ t : T ->
-      Γ ⊢ a_sub t (σ ∙ τ) ≈ a_sub (a_sub t σ) τ : a_sub T (σ ∙ τ)
-    )
-  | wf_eq_var_ze : `(
-      Γ ⊢s σ : Δ ->
-      Δ ⊢ T : typ i ->
-      Γ ⊢ t : a_sub T σ ->
-      Γ ⊢ a_sub (a_var 0) (σ ,, t) ≈ t : a_sub T σ
-    )
-  | wf_eq_var_su : `(
-      Γ ⊢s σ : Δ ->
-      Δ ⊢ T : typ i ->
-      Γ ⊢ t : a_sub T σ ->
-      x : T ∈! Δ ->
-      Γ ⊢ a_sub (a_var (S x)) (σ ,, t) ≈ a_sub (a_var x) σ : a_sub T σ
-    )
-  | wf_eq_cumu :
-      `(Γ ⊢ T ≈ T' : typ i ->Γ ⊢ T ≈ T' : typ (1+i))
-  | wf_eq_conv : `(
-      Γ ⊢ t ≈ t' : T ->
-      Γ ⊢ T ≈ T' : typ i ->
-      Γ ⊢ t ≈ t' : T'
-    )
-  | wf_eq_sym :
-      `(Γ ⊢ t ≈ t' : T -> Γ ⊢ t' ≈ t : T)
-  | wf_eq_trans : `(
-      Γ ⊢ t ≈ t' : T ->
-      Γ ⊢ t' ≈ t'' : T ->
-      Γ ⊢ t ≈ t'' : T
-    )
-where "Γ ⊢ A ≈ B : T" := (wf_term_eq Γ A B T)
-with wf_sub_eq : Ctx -> Sb -> Sb -> Ctx -> Prop :=
-  | wf_sub_eq_id :
-      `(⊢ Γ -> Γ ⊢s a_id ≈ a_id : Γ)
-  | wf_sub_eq_wk :
-      `(⊢ T :: Γ -> T :: Γ ⊢s a_weaken ≈ a_weaken : Γ)
-  | wf_sub_eq_comp_cong : `(
-      Γ ⊢s τ ≈ τ' : Γ' ->
-      Γ' ⊢s σ ≈ σ' : Γ'' ->
-      Γ ⊢s σ ∙ τ ≈ σ' ∙ τ' : Γ''
-    )
-  | wf_sub_eq_ext_cong : `(
-      Γ ⊢s σ ≈ σ' : Δ ->
-      Δ ⊢ T : typ i ->
-      Γ ⊢ t ≈ t' : a_sub T σ ->
-      Γ ⊢s (σ ,, t) ≈ (σ' ,, t') : T :: Δ
-    )
-  | wf_sub_eq_id_comp_right :
-      `(Γ ⊢s σ : Δ -> Γ ⊢s a_id ∙ σ ≈ σ : Δ)
-  | wf_sub_eq_id_comp_left :
-      `(Γ ⊢s σ : Δ -> Γ ⊢s σ ∙ a_id ≈ σ : Δ)
-  | wf_sub_eq_comp_assoc : `(
-      Γ' ⊢s σ : Γ ->
-      Γ'' ⊢s σ' : Γ' ->
-      Γ''' ⊢s σ'' : Γ'' ->
-      Γ''' ⊢s (σ ∙ σ') ∙ σ'' ≈ σ ∙ (σ' ∙ σ'') : Γ
-    )
-  | wf_sub_eq_ext_comp : `(
-      Γ' ⊢s σ : Γ'' ->
-      Γ'' ⊢ T : typ i ->
-      Γ' ⊢ t : a_sub T σ ->
-      Γ ⊢s τ : Γ' ->
-      Γ ⊢s (σ ,, t) ∙ τ ≈ ((σ ∙ τ) ,, (a_sub t τ)) : T :: Γ''
-    )
-  | wf_sub_eq_p_ext : `(
-      Γ' ⊢s σ : Γ ->
-      Γ ⊢ T : typ i ->
-      Γ' ⊢ t : a_sub T σ ->
-      Γ' ⊢s a_weaken ∙ (σ ,, t) ≈ σ : Γ
-    )
-  | wf_sub_eq_ext : `(
-      Γ' ⊢s σ : T :: Γ ->
-      Γ' ⊢s σ ≈ ((a_weaken ∙ σ) ,, (a_sub (a_var 0) σ)) : T :: Γ
-    )
-  | wf_sub_eq_sym :
-      `(Γ ⊢s σ ≈ σ' : Δ -> Γ ⊢s σ' ≈ σ : Δ)
-  | wf_sub_eq_trans : `(
-      Γ ⊢s σ ≈ σ' : Δ ->
-      Γ ⊢s σ' ≈ σ'' : Δ ->
-      Γ ⊢s σ ≈ σ'' : Δ
-    )
-  | wf_sub_eq_conv: `(
-      Γ ⊢s σ ≈ σ' : Δ ->
-      ⊢ Δ ≈ Δ' ->
-      Γ ⊢s σ ≈ σ' : Δ'
-   )
-where "Γ ⊢s S1 ≈ S2 : Δ" := (wf_sub_eq Γ S1 S2 Δ).
+Inductive ctx_lookup : nat -> typ -> ctx -> Prop :=
+  | here : `({{ #0 : T[Wk] ∈ Γ , T }})
+  | there : `({{ #n : T ∈ Γ }} -> {{ #(S n) : T[Wk] ∈ Γ , T' }})
+where "'#' x : T ∈ Γ" := (ctx_lookup x T Γ) (in custom judg) : type_scope.
 
+Inductive wf_ctx : ctx -> Prop :=
+| wf_ctx_empty : {{ ⊢ ⋅ }}
+| wf_ctx_extend :
+  `( {{ ⊢ Γ }} ->
+     {{ Γ ⊢ T : Type@i }} ->
+     {{ ⊢ Γ , T }} )
+where "⊢ Γ" := (wf_ctx Γ) (in custom judg) : type_scope
+with wf_ctx_eq : ctx -> ctx -> Prop :=
+| wf_ctx_eq_empty : {{ ⊢ ⋅ ≈ ⋅ }}
+| wf_ctx_eq_extend :
+  `( {{ ⊢ Γ ≈ Δ }} ->
+     {{ Γ ⊢ T : Type@i }} ->
+     {{ Δ ⊢ T' : Type@i }} ->
+     {{ Γ ⊢ T ≈ T' : Type@i }} ->
+     {{ Δ ⊢ T ≈ T' : Type@i }} ->
+     {{ ⊢ Γ , T ≈ Δ , T' }} )
+where "⊢ Γ ≈ Δ" := (wf_ctx_eq Γ Δ) (in custom judg) : type_scope
+with wf_exp : ctx -> exp -> typ -> Prop :=
+| wf_nat :
+  `( {{ ⊢ Γ }} ->
+     {{ Γ ⊢ ℕ : Type@i }} )
+| wf_univ :
+  `( {{ ⊢ Γ }} ->
+     {{ Γ ⊢ Type@i : Type@(S i) }} )
+| wf_pi :
+  `( {{ Γ ⊢ A : Type@i }} ->
+     {{ Γ , A ⊢ B : Type@i }} ->
+     {{ Γ ⊢ Π A B : Type@i }} )
+| wf_vlookup :
+  `( {{ ⊢ Γ }} ->
+     {{ #x : T ∈ Γ }} ->
+     {{ Γ ⊢ #x : T }} )
+| wf_app :
+  `( {{ Γ ⊢ A : Type@i }} ->
+     {{ Γ , A ⊢ B : Type@i }} ->
+     {{ Γ ⊢ M : Π A B }} ->
+     {{ Γ ⊢ N : A }} ->
+     {{ Γ ⊢ M N : B[Id,,N] }} )
+| wf_fn :
+  `( {{ Γ ⊢ A : Type@i }} ->
+     {{ Γ , A ⊢ M : B }} ->
+     {{ Γ ⊢ λ A M : Π A B }} )
+| wf_zero :
+  `( {{ ⊢ Γ }} ->
+     {{ Γ ⊢ zero : ℕ }} )
+| wf_succ :
+  `( {{ Γ ⊢ n : ℕ }} ->
+     {{ Γ ⊢ succ n : ℕ }} )
+| wf_exp_sub :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Δ ⊢ M : A }} ->
+     {{ Γ ⊢ M[σ] : A[σ] }} )
+| wf_conv :
+  `( {{ Γ ⊢ t : T }} ->
+     {{ Γ ⊢ T ≈ T' : Type@i }} ->
+     {{ Γ ⊢ t : T' }} )
+| wf_cumu :
+  `( {{ Γ ⊢ T : Type@i }} ->
+     {{ Γ ⊢ T : Type@(S i) }} )
+where "Γ ⊢ t : T" := (wf_exp Γ t T) (in custom judg) : type_scope
+with wf_sub : ctx -> sub -> ctx -> Prop :=
+| wf_sub_id :
+  `( {{ ⊢ Γ }} ->
+     {{ Γ ⊢s Id : Γ }} )
+| wf_sub_weaken :
+  `( {{ ⊢ Γ , A }} ->
+     {{ Γ , A ⊢s Wk : Γ }} )
+| wf_sub_compose :
+  `( {{ Γ1 ⊢s σ2 : Γ2 }} ->
+     {{ Γ2 ⊢s σ1 : Γ3 }} ->
+     {{ Γ1 ⊢s σ1 ∘ σ2 : Γ3 }} )
+| wf_sub_extend :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Δ ⊢ A : Type@i }} ->
+     {{ Γ ⊢ M : A[σ] }} ->
+     {{ Γ ⊢s (σ ,, M) : Δ , A }} )
+| wf_sub_conv :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ ⊢ Δ ≈ Δ' }} ->
+     {{ Γ ⊢s σ : Δ' }} )
+where "Γ ⊢s σ : Δ" := (wf_sub Γ σ Δ) (in custom judg) : type_scope
+with wf_eq : ctx -> exp -> exp -> typ -> Prop :=
+| wf_eq_nat_sub :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Γ ⊢ ℕ[σ] ≈ ℕ : Type@i }} )
+| wf_eq_typ_sub :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Γ ⊢ Type@i[σ] ≈ Type@i : Type@(S i) }} )
+| wf_eq_pi_sub :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Δ ⊢ T' : Type@i }} ->
+     {{ Δ , T' ⊢ T : Type@i }} ->
+     {{ Γ ⊢ (Π T' T)[σ] ≈ Π (T'[σ]) (T[σ ∘ Wk ,, #0]) : Type@i }} )
+| wf_eq_pi_cong :
+  `( {{ Γ ⊢ M : Type@i }} ->
+     {{ Γ ⊢ M ≈ M' : Type@i }} ->
+     {{ Γ , M ⊢ T ≈ T' : Type@i }} ->
+     {{ Γ ⊢ Π M T ≈ Π M' T' : Type@i }} )
+| wf_eq_var :
+  `( {{ ⊢ Γ }} ->
+     {{ #x : T ∈ Γ }} ->
+     {{ Γ ⊢ #x ≈ #x : T }} )
+| wf_eq_zero :
+  `( {{ ⊢ Γ }} ->
+     {{ Γ ⊢ zero ≈ zero : ℕ }} )
+| wf_eq_zero_sub :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Γ ⊢ zero[σ] ≈ zero : ℕ }} )
+| wf_eq_succ_cong :
+  `( {{ Γ ⊢ t ≈ t' : ℕ }} ->
+     {{ Γ ⊢ succ t ≈ succ t' : ℕ }} )
+| wf_eq_succ_sub :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Δ ⊢ t : ℕ }} ->
+     {{ Γ ⊢ (succ t)[σ] ≈ succ (t[σ]) : ℕ }} )
+| wf_eq_exp_sub_cong :
+  `( {{ Δ ⊢ t ≈ t' : T }} ->
+     {{ Γ ⊢s σ ≈ σ' : Δ }} ->
+     {{ Γ ⊢ t[σ] ≈ t'[σ'] : T[σ] }} )
+| wf_eq_exp_sub_id :
+  `( {{ Γ ⊢ t : T }} ->
+     {{ Γ ⊢ t[Id] ≈ t : T }} )
+| wf_eq_exp_sub_weaken :
+  `( {{ ⊢ Γ , M }} ->
+     {{ #x : T ∈ Γ }} ->
+     {{ Γ , M ⊢ (#x)[Wk] ≈ #(S x) : T[Wk] }} )
+| wf_eq_exp_sub_compose :
+  `( {{ Γ ⊢s τ : Γ' }} ->
+     {{ Γ' ⊢s σ : Γ'' }} ->
+     {{ Γ'' ⊢ t : T }} ->
+     {{ Γ ⊢ t[σ ∘ τ] ≈ t[σ][τ] : T[σ ∘ τ] }} )
+| wf_eq_var_0_sub :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Δ ⊢ T : Type@i }} ->
+     {{ Γ ⊢ t : T[σ] }} ->
+     {{ Γ ⊢ (#0)[σ ,, t] ≈ t : T[σ] }} )
+| wf_eq_var_S_sub :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Δ ⊢ T : Type@i }} ->
+     {{ Γ ⊢ t : T[σ] }} ->
+     {{ #x : T ∈ Δ }} ->
+     {{ Γ ⊢ (#(S x))[σ ,, t] ≈ (#x)[σ] : T[σ] }} )
+| wf_eq_cumu :
+  `( {{ Γ ⊢ T ≈ T' : Type@i }} ->
+     {{ Γ ⊢ T ≈ T' : Type@(S i) }} )
+| wf_eq_conv :
+  `( {{ Γ ⊢ t ≈ t' : T }} ->
+     {{ Γ ⊢ T ≈ T' : Type@i }} ->
+     {{ Γ ⊢ t ≈ t' : T' }} )
+| wf_eq_sym :
+  `( {{ Γ ⊢ t ≈ t' : T }} ->
+     {{ Γ ⊢ t' ≈ t : T }} )
+| wf_eq_trans :
+  `( {{ Γ ⊢ t ≈ t' : T }} ->
+     {{ Γ ⊢ t' ≈ t'' : T }} ->
+     {{ Γ ⊢ t ≈ t'' : T }} )
+where "Γ ⊢ A ≈ B : T" := (wf_eq Γ A B T) (in custom judg) : type_scope
+with wf_sub_eq : ctx -> sub -> sub -> ctx -> Prop :=
+| wf_sub_eq_id :
+  `( {{ ⊢ Γ }} ->
+     {{ Γ ⊢s Id ≈ Id : Γ }} )
+| wf_sub_eq_weaken :
+  `( {{ ⊢ Γ , T }} ->
+     {{ Γ , T ⊢s Wk ≈ Wk : Γ }} )
+| wf_sub_eq_compose_cong :
+  `( {{ Γ ⊢s τ ≈ τ' : Γ' }} ->
+     {{ Γ' ⊢s σ ≈ σ' : Γ'' }} ->
+     {{ Γ ⊢s σ ∘ τ ≈ σ' ∘ τ' : Γ'' }} )
+| wf_sub_eq_extend_cong :
+  `( {{ Γ ⊢s σ ≈ σ' : Δ }} ->
+     {{ Δ ⊢ T : Type@i }} ->
+     {{ Γ ⊢ t ≈ t' : T[σ] }} ->
+     {{ Γ ⊢s (σ ,, t) ≈ (σ' ,, t') : Δ , T }} )
+| wf_sub_eq_id_compose_right :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Γ ⊢s Id ∘ σ ≈ σ : Δ }} )
+| wf_sub_eq_id_compose_left :
+  `( {{ Γ ⊢s σ : Δ }} ->
+     {{ Γ ⊢s σ ∘ Id ≈ σ : Δ }} )
+| wf_sub_eq_compose_assoc :
+  `( {{ Γ' ⊢s σ : Γ }} ->
+     {{ Γ'' ⊢s σ' : Γ' }} ->
+     {{ Γ''' ⊢s σ'' : Γ'' }} ->
+     {{ Γ''' ⊢s (σ ∘ σ') ∘ σ'' ≈ σ ∘ (σ' ∘ σ'') : Γ }} )
+| wf_sub_eq_extend_compose :
+  `( {{ Γ' ⊢s σ : Γ'' }} ->
+     {{ Γ'' ⊢ T : Type@i }} ->
+     {{ Γ' ⊢ t : T[σ] }} ->
+     {{ Γ ⊢s τ : Γ' }} ->
+     {{ Γ ⊢s (σ ,, t) ∘ τ ≈ ((σ ∘ τ) ,, t[τ]) : Γ'' , T }} )
+| wf_sub_eq_p_extend :
+  `( {{ Γ' ⊢s σ : Γ }} ->
+     {{ Γ ⊢ T : Type@i }} ->
+     {{ Γ' ⊢ t : T[σ] }} ->
+     {{ Γ' ⊢s Wk ∘ (σ ,, t) ≈ σ : Γ }} )
+| wf_sub_eq_extend :
+  `( {{ Γ' ⊢s σ : Γ , T }} ->
+     {{ Γ' ⊢s σ ≈ ((Wk ∘ σ) ,, (#0)[σ]) : Γ , T }} )
+| wf_sub_eq_sym :
+  `( {{ Γ ⊢s σ ≈ σ' : Δ }} ->
+     {{ Γ ⊢s σ' ≈ σ : Δ }} )
+| wf_sub_eq_trans :
+  `( {{ Γ ⊢s σ ≈ σ' : Δ }} ->
+     {{ Γ ⊢s σ' ≈ σ'' : Δ }} ->
+     {{ Γ ⊢s σ ≈ σ'' : Δ }} )
+| wf_sub_eq_conv :
+  `( {{ Γ ⊢s σ ≈ σ' : Δ }} ->
+     {{ ⊢ Δ ≈ Δ' }} ->
+     {{ Γ ⊢s σ ≈ σ' : Δ' }} )
+where "Γ ⊢s S1 ≈ S2 : Δ" := (wf_sub_eq Γ S1 S2 Δ) (in custom judg) : type_scope.
 
 #[export]
-Hint Constructors wf_ctx wf_ctx_eq wf_term wf_sb wf_term_eq wf_sub_eq ctx_lookup: mcltt.
+Hint Constructors wf_ctx wf_ctx_eq wf_exp wf_sub wf_eq wf_sub_eq ctx_lookup: mcltt.