diff --git a/GroupoidModel/Syntax/Autosubst.lean b/GroupoidModel/Syntax/Autosubst.lean
index 559f8235..7cc9105a 100644
--- a/GroupoidModel/Syntax/Autosubst.lean
+++ b/GroupoidModel/Syntax/Autosubst.lean
@@ -41,14 +41,14 @@ def rename (ξ : Nat → Nat) : Expr → Expr
   | .pi l l' A B => .pi l l' (A.rename ξ) (B.rename (upr ξ))
   | .sigma l l' A B => .sigma l l' (A.rename ξ) (B.rename (upr ξ))
   | .lam l l' A t => .lam l l' (A.rename ξ) (t.rename (upr ξ))
-  | .app l l' B fn arg => .app l l' (B.rename (upr ξ)) (fn.rename ξ) (arg.rename ξ)
+  | .app l B fn arg => .app l (B.rename (upr ξ)) (fn.rename ξ) (arg.rename ξ)
   | .pair l l' B t u => .pair l l' (B.rename (upr ξ)) (t.rename ξ) (u.rename ξ)
   | .fst l l' A B p => .fst l l' (A.rename ξ) (B.rename (upr ξ)) (p.rename ξ)
   | .snd l l' A B p => .snd l l' (A.rename ξ) (B.rename (upr ξ)) (p.rename ξ)
-  | .Id l A t u => .Id l (A.rename ξ) (t.rename ξ) (u.rename ξ)
-  | .refl l t => .refl l (t.rename ξ)
-  | .idRec l l' t C r u h =>
-    .idRec l l' (t.rename ξ) (C.rename (upr <| upr ξ)) (r.rename ξ) (u.rename ξ) (h.rename ξ)
+  | .Id A t u => .Id (A.rename ξ) (t.rename ξ) (u.rename ξ)
+  | .refl t => .refl (t.rename ξ)
+  | .idRec l t C r u h =>
+    .idRec l (t.rename ξ) (C.rename (upr <| upr ξ)) (r.rename ξ) (u.rename ξ) (h.rename ξ)
   | .univ l => .univ l
   | .el a => .el (a.rename ξ)
   | .code A => .code (A.rename ξ)
@@ -79,14 +79,14 @@ def subst (σ : Nat → Expr) : Expr → Expr
   | .pi l l' A B => .pi l l' (A.subst σ) (B.subst (up σ))
   | .sigma l l' A B => .sigma l l' (A.subst σ) (B.subst (up σ))
   | .lam l l' A t => .lam l l' (A.subst σ) (t.subst (up σ))
-  | .app l l' B fn arg => .app l l' (B.subst (up σ)) (fn.subst σ) (arg.subst σ)
+  | .app l B fn arg => .app l (B.subst (up σ)) (fn.subst σ) (arg.subst σ)
   | .pair l l' B t u => .pair l l' (B.subst (up σ)) (t.subst σ) (u.subst σ)
   | .fst l l' A B p => .fst l l' (A.subst σ) (B.subst (up σ)) (p.subst σ)
   | .snd l l' A B p => .snd l l' (A.subst σ) (B.subst (up σ)) (p.subst σ)
-  | .Id l A t u => .Id l (A.subst σ) (t.subst σ) (u.subst σ)
-  | .refl l t => .refl l (t.subst σ)
-  | .idRec l l' t C r u h =>
-    .idRec l l' (t.subst σ) (C.subst <| up <| up σ) (r.subst σ) (u.subst σ) (h.subst σ)
+  | .Id A t u => .Id (A.subst σ) (t.subst σ) (u.subst σ)
+  | .refl t => .refl (t.subst σ)
+  | .idRec l t C r u h =>
+    .idRec l (t.subst σ) (C.subst <| up <| up σ) (r.subst σ) (u.subst σ) (h.subst σ)
   | .univ l => .univ l
   | .el a => .el (a.subst σ)
   | .code A => .code (A.subst σ)
diff --git a/GroupoidModel/Syntax/Basic.lean b/GroupoidModel/Syntax/Basic.lean
index c3670f17..4c7c7390 100644
--- a/GroupoidModel/Syntax/Basic.lean
+++ b/GroupoidModel/Syntax/Basic.lean
@@ -9,7 +9,7 @@ inductive Expr where
   /-- Lambda with the specified argument type. -/
   | lam (l l' : Nat) (A b : Expr)
   /-- Application at the specified output type family `B`. -/
-  | app (l l' : Nat) (B fn arg : Expr)
+  | app (l : Nat) (B fn arg : Expr)
   /-- Dependent sum. -/
   | sigma (l l' : Nat) (A B : Expr)
   /-- Pair formation. -/
@@ -20,11 +20,11 @@ inductive Expr where
   | snd (l l' : Nat) (A B p : Expr)
   /-- Identity type. -/
   -- TODO: capitalize all the types
-  | Id (l : Nat) (A t u : Expr)
+  | Id (A t u : Expr)
   /-- A reflexive identity. -/
-  | refl (l : Nat) (t : Expr)
+  | refl (t : Expr)
   /-- Eliminates an identity. -/
-  | idRec (l l' : Nat) (t C r u h : Expr)
+  | idRec (l : Nat) (t C r u h : Expr)
   /-- A type universe. -/
   | univ (l : Nat)
   /-- Type from a code. -/
diff --git a/GroupoidModel/Syntax/GCongr.lean b/GroupoidModel/Syntax/GCongr.lean
index d50a9577..b48d5b93 100644
--- a/GroupoidModel/Syntax/GCongr.lean
+++ b/GroupoidModel/Syntax/GCongr.lean
@@ -55,21 +55,21 @@ theorem EqTp.cong_Id_tp {Γ A A' t u l} :
     Γ ⊢[l] A ≡ A' →
     Γ ⊢[l] t : A →
     Γ ⊢[l] u : A →
-    Γ ⊢[l] .Id l A t u ≡ .Id l A' t u :=
+    Γ ⊢[l] .Id A t u ≡ .Id A' t u :=
   fun A t u => .cong_Id A (.refl_tm t) (.refl_tm u)
 
 @[gcongr]
 theorem EqTp.cong_Id_left {Γ A t t' u l} :
     Γ ⊢[l] t ≡ t' : A →
     Γ ⊢[l] u : A →
-    Γ ⊢[l] .Id l A t u ≡ .Id l A t' u :=
+    Γ ⊢[l] .Id A t u ≡ .Id A t' u :=
   fun h h' => .cong_Id (.refl_tp h.wf_tp) h (.refl_tm h')
 
 @[gcongr]
 theorem EqTp.cong_Id_right {Γ A t u u' l} :
     Γ ⊢[l] t : A →
     Γ ⊢[l] u ≡ u' : A →
-    Γ ⊢[l] .Id l A t u ≡ .Id l A t u' :=
+    Γ ⊢[l] .Id A t u ≡ .Id A t u' :=
   fun h h' => .cong_Id (.refl_tp h.wf_tp) (.refl_tm h) h'
 
 attribute [gcongr] EqTp.cong_Id
@@ -98,7 +98,7 @@ theorem EqTm.cong_app_cod {Γ A B B' f a l l'} :
     (A, l) :: Γ ⊢[l'] B ≡ B' →
     Γ ⊢[max l l'] f : .pi l l' A B →
     Γ ⊢[l] a : A →
-    Γ ⊢[l'] .app l l' B f a ≡ .app l l' B' f a : B.subst a.toSb :=
+    Γ ⊢[l'] .app l B f a ≡ .app l B' f a : B.subst a.toSb :=
   fun hBB' hf ha =>
     EqTm.cong_app hBB' (EqTm.refl_tm hf) (EqTm.refl_tm ha)
 
@@ -106,7 +106,7 @@ theorem EqTm.cong_app_cod {Γ A B B' f a l l'} :
 theorem EqTm.cong_app_fn {Γ A B f f' a l l'} :
     Γ ⊢[max l l'] f ≡ f' : .pi l l' A B →
     Γ ⊢[l] a : A →
-    Γ ⊢[l'] .app l l' B f a ≡ .app l l' B f' a : B.subst a.toSb :=
+    Γ ⊢[l'] .app l B f a ≡ .app l B f' a : B.subst a.toSb :=
   fun hff' ha =>
     EqTm.cong_app (EqTp.refl_tp hff'.wf_tp.inv_pi.2) hff' (EqTm.refl_tm ha)
 
@@ -114,7 +114,7 @@ theorem EqTm.cong_app_fn {Γ A B f f' a l l'} :
 theorem EqTm.cong_app_arg {Γ A B f a a' l l'} :
     Γ ⊢[max l l'] f : .pi l l' A B →
     Γ ⊢[l] a ≡ a' : A →
-    Γ ⊢[l'] .app l l' B f a ≡ .app l l' B f a' : B.subst a.toSb :=
+    Γ ⊢[l'] .app l B f a ≡ .app l B f a' : B.subst a.toSb :=
   fun hf haa' =>
     EqTm.cong_app (EqTp.refl_tp hf.wf_tp.inv_pi.2) (EqTm.refl_tm hf) haa'
 
diff --git a/GroupoidModel/Syntax/Injectivity.lean b/GroupoidModel/Syntax/Injectivity.lean
index c2ddf67d..2d39a9d8 100644
--- a/GroupoidModel/Syntax/Injectivity.lean
+++ b/GroupoidModel/Syntax/Injectivity.lean
@@ -18,6 +18,6 @@ axiom EqTp.inv_sigma {Γ A B A' B' l₀ l₁ l₂ l₁' l₂'} :
     (Γ ⊢[l₁] A ≡ A') ∧ ((A, l₁) :: Γ ⊢[l₂] B ≡ B')
 
 /-- Injectivity of Id types. -/
-axiom EqTp.inv_Id {Γ A A' t u t' u' l₀ l l'} :
-    Γ ⊢[l₀] .Id l A t u ≡ .Id l' A' t' u' →
-    l₀ = l ∧ l₀ = l' ∧ (Γ ⊢[l₀] A ≡ A') ∧ (Γ ⊢[l₀] t ≡ t' : A) ∧ (Γ ⊢[l₀] u ≡ u' : A)
+axiom EqTp.inv_Id {Γ A A' t u t' u' l} :
+    Γ ⊢[l] .Id A t u ≡ .Id A' t' u' →
+    (Γ ⊢[l] A ≡ A') ∧ (Γ ⊢[l] t ≡ t' : A) ∧ (Γ ⊢[l] u ≡ u' : A)
diff --git a/GroupoidModel/Syntax/Interpretation.lean b/GroupoidModel/Syntax/Interpretation.lean
index 87daa40b..04ca3ba1 100644
--- a/GroupoidModel/Syntax/Interpretation.lean
+++ b/GroupoidModel/Syntax/Interpretation.lean
@@ -291,7 +291,7 @@ def ofType (Γ : s.CObj) (l : Nat) :
     let A ← ofType Γ i A
     let B ← ofType (Γ.snoc ilen A) j B
     return lij ▸ s.mkSigma ilen jlen A B
-  | .Id _ A a0 a1, llen => do
+  | .Id A a0 a1, llen => do
     let A ← ofType Γ l A
     let a0 ← ofTerm Γ l a0
     let a1 ← ofTerm Γ l a1
@@ -318,15 +318,14 @@ def ofTerm (Γ : s.CObj) (l : Nat) :
     let A ← ofType Γ i A
     let e ← ofTerm (Γ.snoc ilen A) j e
     return lij ▸ s.mkLam ilen jlen A e
-  | .app i j B f a, _ => do
-    Part.assert (l = j) fun lj => do
+  | .app i B f a, llen => do
     Part.assert (i < s.length + 1) fun ilen => do
-    have jlen : j < s.length + 1 := by omega
-    let f ← ofTerm Γ (max i j) f
+    have jlen : l < s.length + 1 := by omega
+    let f ← ofTerm Γ (max i l) f
     let a ← ofTerm Γ i a
-    let B ← ofType (Γ.snoc ilen (a ≫ s[i].tp)) j B
-    Part.assert (f ≫ s[max i j].tp = s.mkPi ilen jlen (a ≫ s[i].tp) B) fun h =>
-    return lj ▸ s.mkApp ilen jlen _ B f h a rfl
+    let B ← ofType (Γ.snoc ilen (a ≫ s[i].tp)) l B
+    Part.assert (f ≫ s[max i l].tp = s.mkPi ilen llen (a ≫ s[i].tp) B) fun h =>
+    return s.mkApp ilen llen _ B f h a rfl
   | .pair i j B t u, _ => do
     Part.assert (l = max i j) fun lij => do
     have ilen : i < s.length + 1 := by omega
@@ -394,8 +393,8 @@ theorem mem_ofType_sigma {Γ l i j A B} {llen : l < s.length + 1} {x} :
   dsimp only [ofType]; simp_part; exact exists_congr fun _ => by subst l; simp_part
 
 @[simp]
-theorem mem_ofType_Id {Γ l i A a b} {llen : l < s.length + 1} {x} :
-    x ∈ s.ofType Γ l (.Id i A a b) llen ↔
+theorem mem_ofType_Id {Γ l A a b} {llen : l < s.length + 1} {x} :
+    x ∈ s.ofType Γ l (.Id A a b) llen ↔
     ∃ (A' : y(Γ.fst) ⟶ s[l].Ty), A' ∈ s.ofType Γ l A ∧
     ∃ (a' : y(Γ.fst) ⟶ s[l].Tm), a' ∈ s.ofTerm Γ l a ∧
     ∃ (b' : y(Γ.fst) ⟶ s[l].Tm), b' ∈ s.ofTerm Γ l b ∧
@@ -443,17 +442,16 @@ theorem mem_ofTerm_lam {Γ l i j A e} {llen : l < s.length + 1} {x} :
   dsimp only [ofTerm]; simp_part; exact exists_congr fun _ => by subst l; simp_part
 
 @[simp]
-theorem mem_ofTerm_app {Γ l i j B f a} {llen : l < s.length + 1} {x} :
-    x ∈ s.ofTerm Γ l (.app i j B f a) llen ↔
-    ∃ lj : l = j,
+theorem mem_ofTerm_app {Γ l i B f a} {llen : l < s.length + 1} {x} :
+    x ∈ s.ofTerm Γ l (.app i B f a) llen ↔
     ∃ ilen : i < s.length + 1,
-    have jlen : j < s.length + 1 := by omega
-    ∃ f' : y(Γ.1) ⟶ s[max i j].Tm, f' ∈ ofTerm Γ (max i j) f ∧
+    have llen : l < s.length + 1 := by omega
+    ∃ f' : y(Γ.1) ⟶ s[max i l].Tm, f' ∈ ofTerm Γ (max i l) f ∧
     ∃ a' : y(Γ.1) ⟶ s[i].Tm, a' ∈ ofTerm Γ i a ∧
-    ∃ B' : y((Γ.snoc ilen (a' ≫ s[i].tp)).1) ⟶ s[j].Ty,
-      B' ∈ ofType (Γ.snoc ilen (a' ≫ s[i].tp)) j B ∧
-    ∃ h, x = lj ▸ s.mkApp ilen jlen _ B' f' h a' rfl := by
-  dsimp only [ofTerm]; simp_part; exact exists_congr fun _ => by subst l; simp_part
+    ∃ B' : y((Γ.snoc ilen (a' ≫ s[i].tp)).1) ⟶ s[l].Ty,
+      B' ∈ ofType (Γ.snoc ilen (a' ≫ s[i].tp)) l B ∧
+    ∃ h, x = s.mkApp ilen llen _ B' f' h a' rfl := by
+  dsimp only [ofTerm]; simp_part
 
 @[simp]
 theorem mem_ofTerm_pair {Γ l i j B t u} {llen : l < s.length + 1} {x} :
@@ -667,9 +665,8 @@ theorem mem_ofType_ofTerm_subst' {full}
     refine ⟨_, (ihA llen.1 σ).1 hA, _, ?_, rfl⟩
     rw [← CSb.up_toSb]; exact (ihB llen.2 (σ.up llen.1 A)).2 hB
   case app ihB ihf iha =>
-    obtain ⟨rfl, llen', H⟩ := mem_ofTerm_app.1 H; simp at H llen
-    obtain ⟨f, hf, a, ha, B, hB, eq, rfl⟩ := H; clear H
-    simp only [Expr.subst, comp_mkApp, mem_ofTerm_app, exists_true_left]
+    obtain ⟨llen', f, hf, a, ha, B, hB, eq, rfl⟩ := mem_ofTerm_app.1 H
+    simp only [Expr.subst, comp_mkApp, mem_ofTerm_app]
     refine ⟨‹_›, _, (ihf (by simp [*]) σ).2 hf, _, (iha llen' σ).2 ha, _, ?_, ?_, rfl⟩
     · rw [← CSb.up'_toSb]; exact (ihB llen (σ.up' llen' _ (Category.assoc ..).symm)).1 hB
     · simp [*, comp_mkPi]
diff --git a/GroupoidModel/Syntax/Inversion.lean b/GroupoidModel/Syntax/Inversion.lean
index e31533a7..72650097 100644
--- a/GroupoidModel/Syntax/Inversion.lean
+++ b/GroupoidModel/Syntax/Inversion.lean
@@ -292,11 +292,11 @@ theorem WfTp.inv_sigma {Γ A B l₀ l l'} : Γ ⊢[l₀] .sigma l l' A B →
     fun h => this h rfl
   mutual_induction WfCtx <;> grind
 
-theorem WfTp.inv_Id {Γ A t u l₀ l} : Γ ⊢[l₀] .Id l A t u →
-    l₀ = l ∧ (Γ ⊢[l] t : A) ∧ (Γ ⊢[l] u : A) := by
+theorem WfTp.inv_Id {Γ A t u l} : Γ ⊢[l] .Id A t u →
+    (Γ ⊢[l] t : A) ∧ (Γ ⊢[l] u : A) := by
   suffices
-      ∀ {Γ l₀ T}, Γ ⊢[l₀] T → ∀ {l t u}, T = .Id l A t u →
-        l₀ = l ∧ (Γ ⊢[l] t : A) ∧ (Γ ⊢[l] u : A) from
+      ∀ {Γ l T}, Γ ⊢[l] T → ∀ {t u}, T = .Id A t u →
+        (Γ ⊢[l] t : A) ∧ (Γ ⊢[l] u : A) from
     fun h => this h rfl
   mutual_induction WfCtx <;> grind
 
@@ -323,7 +323,7 @@ theorem WfTp.sigma {Γ A B l l'} :
 theorem WfTp.Id {Γ A t u l} :
     Γ ⊢[l] t : A →
     Γ ⊢[l] u : A →
-    Γ ⊢[l] .Id l A t u :=
+    Γ ⊢[l] .Id A t u :=
   fun t u => WfTp.Id' t.wf_tp t u
 
 theorem EqTp.cong_pi {Γ A A' B B' l l'} :
@@ -346,7 +346,7 @@ theorem WfTm.lam {Γ A B t l l'} :
 theorem WfTm.app {Γ A B f a l l'} :
     Γ ⊢[max l l'] f : .pi l l' A B →
     Γ ⊢[l] a : A →
-    Γ ⊢[l'] .app l l' B f a : B.subst a.toSb :=
+    Γ ⊢[l'] .app l B f a : B.subst a.toSb :=
   fun hf ha =>
     have ⟨_, hB⟩ := hf.wf_tp.inv_pi
     WfTm.app' hB.wf_binder hB hf ha
@@ -374,16 +374,16 @@ theorem WfTm.snd {Γ A B p l l'} :
 
 theorem WfTm.refl {Γ A t l} :
     Γ ⊢[l] t : A →
-    Γ ⊢[l] .refl l t : .Id l A t t :=
+    Γ ⊢[l] .refl t : .Id A t t :=
   fun t => .refl' t.wf_tp t
 
 theorem WfTm.idRec {Γ A M t r u h l l'} :
-    (.Id l (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M →
-    Γ ⊢[l'] r : M.subst (.snoc t.toSb <| .refl l t) →
-    Γ ⊢[l] h : .Id l A t u →
-    Γ ⊢[l'] .idRec l l' t M r u h : M.subst (.snoc u.toSb h) :=
+    (.Id (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M →
+    Γ ⊢[l'] r : M.subst (.snoc t.toSb <| .refl t) →
+    Γ ⊢[l] h : .Id A t u →
+    Γ ⊢[l'] .idRec l t M r u h : M.subst (.snoc u.toSb h) :=
   fun M r h =>
-    have ⟨_, t, u⟩ := h.wf_tp.inv_Id
+    have ⟨t, u⟩ := h.wf_tp.inv_Id
     .idRec' t.wf_tp t M r u h
 
 theorem EqTm.cong_lam {Γ A A' B t t' l l'} :
@@ -396,7 +396,7 @@ theorem EqTm.cong_app {Γ A B B' f f' a a' l l'} :
     (A, l) :: Γ ⊢[l'] B ≡ B' →
     Γ ⊢[max l l'] f ≡ f' : .pi l l' A B →
     Γ ⊢[l] a ≡ a' : A →
-    Γ ⊢[l'] .app l l' B f a ≡ .app l l' B' f' a' : B.subst a.toSb :=
+    Γ ⊢[l'] .app l B f a ≡ .app l B' f' a' : B.subst a.toSb :=
   fun hBB' hff' haa' => EqTm.cong_app' haa'.wf_tp hBB' hff' haa'
 
 theorem EqTm.cong_pair {Γ A B B' t t' u u' l l'} :
@@ -422,17 +422,17 @@ theorem EqTm.cong_snd {Γ A A' B B' p p' l l'} :
 
 theorem EqTm.cong_idRec {Γ A M M' t t' r r' u u' h h' l l'} :
     Γ ⊢[l] t ≡ t' : A →
-    (.Id l (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M ≡ M' →
-    Γ ⊢[l'] r ≡ r' : M.subst (.snoc t.toSb <| .refl l t) →
+    (.Id (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M ≡ M' →
+    Γ ⊢[l'] r ≡ r' : M.subst (.snoc t.toSb <| .refl t) →
     Γ ⊢[l] u ≡ u' : A →
-    Γ ⊢[l] h ≡ h' : .Id l A t u →
-    Γ ⊢[l'] .idRec l l' t M r u h ≡ .idRec l l' t' M' r' u' h' : M.subst (.snoc u.toSb h) :=
+    Γ ⊢[l] h ≡ h' : .Id A t u →
+    Γ ⊢[l'] .idRec l t M r u h ≡ .idRec l t' M' r' u' h' : M.subst (.snoc u.toSb h) :=
   fun teq Meq req ueq heq => .cong_idRec' teq.wf_tp teq.wf_left teq Meq req ueq heq
 
 theorem EqTm.app_lam {Γ A B t u l l'} :
     (A, l) :: Γ ⊢[l'] t : B →
     Γ ⊢[l] u : A →
-    Γ ⊢[l'] .app l l' B (.lam l l' A t) u ≡ t.subst u.toSb : B.subst u.toSb :=
+    Γ ⊢[l'] .app l B (.lam l l' A t) u ≡ t.subst u.toSb : B.subst u.toSb :=
   fun ht hu => EqTm.app_lam' hu.wf_tp ht.wf_tp ht hu
 
 theorem EqTm.fst_pair {Γ A B t u l l'} :
@@ -451,20 +451,20 @@ theorem EqTm.snd_pair {Γ A B t u l l'} :
 
 theorem EqTm.cong_refl {Γ A t t' l} :
     Γ ⊢[l] t ≡ t' : A →
-    Γ ⊢[l] .refl l t ≡ .refl l t' : .Id l A t t :=
+    Γ ⊢[l] .refl t ≡ .refl t' : .Id A t t :=
   fun t => .cong_refl' t.wf_tp t
 
 theorem EqTm.idRec_refl {Γ A M t r l l'} :
     Γ ⊢[l] t : A →
-    (.Id l (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M →
-    Γ ⊢[l'] r : M.subst (.snoc t.toSb <| .refl l t) →
-    Γ ⊢[l'] .idRec l l' t M r t (.refl l t) ≡ r : M.subst (.snoc t.toSb <| .refl l t) :=
+    (.Id (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M →
+    Γ ⊢[l'] r : M.subst (.snoc t.toSb <| .refl t) →
+    Γ ⊢[l'] .idRec l t M r t (.refl t) ≡ r : M.subst (.snoc t.toSb <| .refl t) :=
   fun t M r => .idRec_refl' t.wf_tp t M r
 
 theorem EqTm.lam_app {Γ A B f l l'} :
     Γ ⊢[max l l'] f : .pi l l' A B →
     Γ ⊢[max l l'] f ≡
-      .lam l l' A (.app l l' (B.subst (Expr.up Expr.wk)) (f.subst Expr.wk) (.bvar 0)) :
+      .lam l l' A (.app l (B.subst (Expr.up Expr.wk)) (f.subst Expr.wk) (.bvar 0)) :
       .pi l l' A B :=
   fun hf =>
     have ⟨_, hB⟩ := hf.wf_tp.inv_pi
@@ -489,7 +489,7 @@ theorem EqTm.trans_tm {Γ A t t' t'' l} :
   fun htt' ht't'' => EqTm.trans_tm' htt'.wf_tp htt' ht't''
 
 theorem WfTp.Id_bvar {Γ A t l} : Γ ⊢[l] t : A →
-    (A, l) :: Γ ⊢[l] .Id l (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0) :=
+    (A, l) :: Γ ⊢[l] .Id (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0) :=
   fun t => WfTp.Id (t.subst (WfSb.wk t.wf_tp)) (.bvar (t.wf_ctx.snoc t.wf_tp) (.zero ..))
 
 /-! ## Term former inversion -/
@@ -513,13 +513,11 @@ theorem WfTm.inv_lam {Γ A C b l₀ l l'} : Γ ⊢[l₀] .lam l l' A b : C →
   mutual_induction WfCtx <;>
     try grind [WfTp.pi, WfTm.wf_tp, EqTp.refl_tp, EqTp.symm_tp, EqTp.trans_tp]
 
-theorem WfTm.inv_app {Γ B C f a l₀ l l'} : Γ ⊢[l₀] .app l l' B f a : C →
-    l₀ = l' ∧ ∃ A,
-      (Γ ⊢[max l l'] f : .pi l l' A B) ∧ (Γ ⊢[l] a : A) ∧ (Γ ⊢[l'] C ≡ B.subst a.toSb) := by
+theorem WfTm.inv_app {Γ B C f a l l'} : Γ ⊢[l'] .app l B f a : C →
+    ∃ A, (Γ ⊢[max l l'] f : .pi l l' A B) ∧ (Γ ⊢[l] a : A) ∧ (Γ ⊢[l'] C ≡ B.subst a.toSb) := by
   suffices
-      ∀ {Γ l₀ C t}, Γ ⊢[l₀] t : C → ∀ {B f a l l'}, t = .app l l' B f a →
-        l₀ = l' ∧ ∃ A,
-          (Γ ⊢[max l l'] f : .pi l l' A B) ∧ (Γ ⊢[l] a : A) ∧ (Γ ⊢[l'] C ≡ B.subst a.toSb) from
+      ∀ {Γ l' C t}, Γ ⊢[l'] t : C → ∀ {B f a l}, t = .app l B f a →
+        ∃ A, (Γ ⊢[max l l'] f : .pi l l' A B) ∧ (Γ ⊢[l] a : A) ∧ (Γ ⊢[l'] C ≡ B.subst a.toSb) from
     fun h => this h rfl
   mutual_induction WfCtx <;>
     grind [InvProof.tp_inst, WfTp.wf_ctx, EqTp.refl_tp, EqTp.symm_tp, EqTp.trans_tp]
@@ -557,36 +555,36 @@ theorem WfTm.inv_snd {Γ A B C p l₀ l l'} : Γ ⊢[l₀] .snd l l' A B p : C 
   mutual_induction WfCtx <;>
     grind [InvProof.tp_inst, EqTp.refl_tp, EqTp.symm_tp, EqTp.trans_tp, WfTm.fst, WfTp.wf_ctx]
 
-theorem WfTm.inv_refl {Γ C t l₀ l} : Γ ⊢[l₀] .refl l t : C →
-    l₀ = l ∧ ∃ A, (Γ ⊢[l] t : A) ∧ (Γ ⊢[l] C ≡ .Id l A t t) := by
+theorem WfTm.inv_refl {Γ C t l} : Γ ⊢[l] .refl t : C →
+    ∃ A, (Γ ⊢[l] t : A) ∧ (Γ ⊢[l] C ≡ .Id A t t) := by
   suffices
-      ∀ {Γ l₀ C t'}, Γ ⊢[l₀] t' : C → ∀ {l t}, t' = .refl l t →
-        l₀ = l ∧ ∃ A, (Γ ⊢[l] t : A) ∧ (Γ ⊢[l] C ≡ .Id l A t t) from
+      ∀ {Γ l C t'}, Γ ⊢[l] t' : C → ∀ {t}, t' = .refl t →
+        ∃ A, (Γ ⊢[l] t : A) ∧ (Γ ⊢[l] C ≡ .Id A t t) from
     fun h => this h rfl
   mutual_induction WfCtx <;> grind [WfTp.Id,  EqTp.refl_tp, EqTp.symm_tp, EqTp.trans_tp]
 
-theorem WfTm.inv_idRec {Γ M C t r u h l₀ l l'} : Γ ⊢[l₀] .idRec l l' t M r u h : C →
-    l₀ = l' ∧ ∃ A,
+theorem WfTm.inv_idRec {Γ M C t r u h l l'} : Γ ⊢[l'] .idRec l t M r u h : C →
+    ∃ A,
       (Γ ⊢[l] t : A) ∧
-      ((.Id l (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M) ∧
-      (Γ ⊢[l'] r : M.subst (.snoc t.toSb <| .refl l t)) ∧
+      ((.Id (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M) ∧
+      (Γ ⊢[l'] r : M.subst (.snoc t.toSb <| .refl t)) ∧
       (Γ ⊢[l] u : A) ∧
-      (Γ ⊢[l] h : .Id l A t u) ∧
+      (Γ ⊢[l] h : .Id A t u) ∧
       (Γ ⊢[l'] C ≡ M.subst (.snoc u.toSb h)) := by
-  suffices ∀ {Γ l₀ C t'}, Γ ⊢[l₀] t' : C → ∀ {t M r u h l l'}, t' = .idRec l l' t M r u h →
-      l₀ = l' ∧ ∃ A,
+  suffices ∀ {Γ l' C t'}, Γ ⊢[l'] t' : C → ∀ {t M r u h l}, t' = .idRec l t M r u h →
+      ∃ A,
         (Γ ⊢[l] t : A) ∧
-        ((.Id l (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M) ∧
-        (Γ ⊢[l'] r : M.subst (.snoc t.toSb <| .refl l t)) ∧
+        ((.Id (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M) ∧
+        (Γ ⊢[l'] r : M.subst (.snoc t.toSb <| .refl t)) ∧
         (Γ ⊢[l] u : A) ∧
-        (Γ ⊢[l] h : .Id l A t u) ∧
+        (Γ ⊢[l] h : .Id A t u) ∧
         (Γ ⊢[l'] C ≡ M.subst (.snoc u.toSb h)) from
     fun h => this h rfl
   mutual_induction WfCtx
   all_goals intros; try exact True.intro
   all_goals rename_i eq; cases eq
   case refl t M r u h _ _ _ _ _ _ =>
-    refine ⟨rfl, _, t, M, r, u, h, ?_⟩
+    refine ⟨_, t, M, r, u, h, ?_⟩
     apply EqTp.refl_tp <| M.subst (WfSb.snoc (WfSb.toSb u) _ _)
     . grind [WfTp.Id_bvar, WfTp.wf_ctx]
     . autosubst; assumption
diff --git a/GroupoidModel/Syntax/Substitution.lean b/GroupoidModel/Syntax/Substitution.lean
index 8cb65cd7..051c6792 100644
--- a/GroupoidModel/Syntax/Substitution.lean
+++ b/GroupoidModel/Syntax/Substitution.lean
@@ -354,7 +354,7 @@ theorem wfSb_up {Δ Γ A σ l} : WfSb Δ σ Γ →
 
 theorem Id_bvar {Γ A t l} :
     WfCtx Γ → Γ ⊢[l] A → Γ ⊢[l] t : A →
-    (A, l) :: Γ ⊢[l] .Id l (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0) :=
+    (A, l) :: Γ ⊢[l] .Id (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0) :=
   fun Γ A t => WfTp.Id' (tp_wk Γ A A) (tm_wk Γ A t) (.bvar (Γ.snoc A) (.zero ..))
 
 attribute [local grind ←] WfCtx.snoc eqSb_up wfSb_up in
diff --git a/GroupoidModel/Syntax/Synth.lean b/GroupoidModel/Syntax/Synth.lean
index 4ea59d5c..6ea19a74 100644
--- a/GroupoidModel/Syntax/Synth.lean
+++ b/GroupoidModel/Syntax/Synth.lean
@@ -17,11 +17,11 @@ where
   | .pi _ _ A B | .sigma _ _ A B =>
     let l := go Γ A
     max l (go (l :: Γ) B)
-  | .Id _ A _ _ => go Γ A
+  | .Id A _ _ => go Γ A
   | .lam _ _ A b =>
     let l := go Γ A
     max l (go (l :: Γ) b)
-  | .app _ _ B _ a =>
+  | .app _ B _ a =>
     let l := go Γ a
     go (l :: Γ) B
   | .pair _ _ _ t u => max (go Γ t) (go Γ u)
@@ -29,8 +29,8 @@ where
   | .snd _ _ A B _ =>
     let l := go Γ A
     go (l :: Γ) B
-  | .refl _ t => go Γ t
-  | .idRec _ _ _ _ r .. => go Γ r
+  | .refl t => go Γ t
+  | .idRec _ _ _ r .. => go Γ r
   | .univ l => l + 1
   | .el a => go Γ a - 1
   | .code A => go Γ A + 1
@@ -66,12 +66,12 @@ noncomputable def synthTp (Γ : Ctx) : Expr → Expr
   | .bvar 0 => Γ[0]? |>.getD default |>.1.subst Expr.wk
   | .bvar (i+1) => synthTp (Γ.drop 1) (.bvar i) |>.subst Expr.wk
   | .lam l l' A b => .pi l l' A (synthTp ((A, l) :: Γ) b)
-  | .app _ _ B _ a => B.subst a.toSb
+  | .app _ B _ a => B.subst a.toSb
   | .pair l l' B t _ => .sigma l l' (synthTp Γ t) B
   | .fst _ _ A _ _ => A
   | .snd l l' A B p => B.subst (Expr.fst l l' A B p).toSb
-  | .refl l t => .Id l (synthTp Γ t) t t
-  | .idRec _ _ _ M _ u h => M.subst (.snoc u.toSb h)
+  | .refl t => .Id (synthTp Γ t) t t
+  | .idRec _ _ M _ u h => M.subst (.snoc u.toSb h)
   | .code A => .univ (synthLvl Γ A)
   | _ => default
 
diff --git a/GroupoidModel/Syntax/Typechecker/Equate.lean b/GroupoidModel/Syntax/Typechecker/Equate.lean
index 35d26043..9edb4027 100644
--- a/GroupoidModel/Syntax/Typechecker/Equate.lean
+++ b/GroupoidModel/Syntax/Typechecker/Equate.lean
@@ -3,17 +3,17 @@ import GroupoidModel.Syntax.Typechecker.Evaluate
 open Qq
 
 mutual
-partial def equateTp (d : Q(Nat)) (l : Q(Nat)) (vT vU : Q(Val)) :
-    Lean.MetaM Q(∀ {Γ T U},
-      $d = Γ.length → ValEqTp Γ $l $vT T → ValEqTp Γ $l $vU U → Γ ⊢[$l] T ≡ U) := do
+partial def equateTp (d : Q(Nat)) (vT vU : Q(Val)) :
+    Lean.MetaM Q(∀ {Γ l T U},
+      $d = Γ.length → ValEqTp Γ l $vT T → ValEqTp Γ l $vU U → Γ ⊢[l] T ≡ U) := do
   match vT, vU with
   | ~q(.pi $k $k' $vA $vB), ~q(.pi $m $m' $vA' $vB') => do
     let keq ← equateNat q($k) q($m)
     let keq' ← equateNat q($k') q($m')
-    let Aeq ← equateTp q($d) q($k) q($vA) q($vA')
+    let Aeq ← equateTp q($d) q($vA) q($vA')
     let ⟨Bx, Bxpost⟩ ← forceClosTp q($d) q($vA) q($vB)
     let ⟨Bx', Bxpost'⟩ ← forceClosTp q($d) q($vA') q($vB')
-    let Beq ← equateTp q($d + 1) q($k') q($Bx) q($Bx')
+    let Beq ← equateTp q($d + 1) q($Bx) q($Bx')
     return q(by as_aux_lemma =>
       introv _ vT vU
       have ⟨_, _, _, vA, vB, eq⟩ := vT.inv_pi
@@ -29,10 +29,10 @@ partial def equateTp (d : Q(Nat)) (l : Q(Nat)) (vT vU : Q(Val)) :
   | ~q(.sigma $k $k' $vA $vB), ~q(.sigma $m $m' $vA' $vB') => do
     let keq ← equateNat q($k) q($m)
     let keq' ← equateNat q($k') q($m')
-    let Aeq ← equateTp q($d) q($k) q($vA) q($vA')
+    let Aeq ← equateTp q($d) q($vA) q($vA')
     let ⟨Bx, Bxpost⟩ ← forceClosTp q($d) q($vA) q($vB)
     let ⟨Bx', Bxpost'⟩ ← forceClosTp q($d) q($vA') q($vB')
-    let Beq ← equateTp q($d + 1) q($k') q($Bx) q($Bx')
+    let Beq ← equateTp q($d + 1) q($Bx) q($Bx')
     return q(by as_aux_lemma =>
       introv _ vT vU
       have ⟨_, _, _, vA, vB, eq⟩ := vT.inv_sigma
@@ -45,15 +45,14 @@ partial def equateTp (d : Q(Nat)) (l : Q(Nat)) (vT vU : Q(Val)) :
       have := $Beq (by simp) Bx (Bx'.conv_ctx (EqCtx.refl Aeq.wf_ctx |>.snoc Aeq.symm_tp))
       gcongr
     )
-  | ~q(.Id $k $vA $va $vb), ~q(.Id $m $vA' $va' $vb') => do
-    let keq ← equateNat q($k) q($m)
-    let Aeq ← equateTp q($d) q($k) q($vA) q($vA')
-    let aeq ← equateTm q($d) q($k) q($vA) q($va) q($va')
-    let beq ← equateTm q($d) q($k) q($vA) q($vb) q($vb')
+  | ~q(.Id $vA $va $vb), ~q(.Id $vA' $va' $vb') => do
+    let Aeq ← equateTp q($d) q($vA) q($vA')
+    let aeq ← equateTm q($d) q($vA) q($va) q($va')
+    let beq ← equateTm q($d) q($vA) q($vb) q($vb')
     return q(by as_aux_lemma =>
       introv _ vT vU
-      have ⟨_, _, _, _, vA, va, vb, eq⟩ := vT.inv_Id
-      have ⟨_, _, _, _, vA', va', vb', eq'⟩ := vU.inv_Id
+      have ⟨_, _, _, vA, va, vb, eq⟩ := vT.inv_Id
+      have ⟨_, _, _, vA', va', vb', eq'⟩ := vU.inv_Id
       subst_vars
       apply eq.trans_tp _ |>.trans_tp eq'.symm_tp
       have Aeq := $Aeq rfl vA vA'
@@ -85,16 +84,16 @@ partial def equateTp (d : Q(Nat)) (l : Q(Nat)) (vT vU : Q(Val)) :
   | vT, vU =>
     throwError "cannot prove normal types are equal{Lean.indentExpr vT}\n≡?≡{Lean.indentExpr vU}"
 
-partial def equateTm (d : Q(Nat)) (l : Q(Nat)) (vT vt vu : Q(Val)) : Lean.MetaM Q(∀ {Γ T t u},
-    $d = Γ.length → ValEqTp Γ $l $vT T → ValEqTm Γ $l $vt t T → ValEqTm Γ $l $vu u T →
-      Γ ⊢[$l] t ≡ u : T) := do
+partial def equateTm (d : Q(Nat)) (vT vt vu : Q(Val)) : Lean.MetaM Q(∀ {Γ l T t u},
+    $d = Γ.length → ValEqTp Γ l $vT T → ValEqTm Γ l $vt t T → ValEqTm Γ l $vu u T →
+      Γ ⊢[l] t ≡ u : T) := do
   match vT with
   | ~q(.pi _ $k' $vA $vB) => do
     let x : Q(Val) := q(.neut (.bvar $d) $vA)
     let ⟨tx, txpost⟩ ← evalApp q($vt) q($x)
     let ⟨ux, uxpost⟩ ← evalApp q($vu) q($x)
     let ⟨Bx, Bxpost⟩ ← forceClosTp q($d) q($vA) q($vB)
-    let tueq ← equateTm q($d + 1) q($k') q($Bx) q($tx) q($ux)
+    let tueq ← equateTm q($d + 1) q($Bx) q($tx) q($ux)
     return q(by as_aux_lemma =>
       introv _ vT vt vu
       have ⟨_, _, _, vA, vB, eq⟩ := vT.inv_pi
@@ -120,11 +119,11 @@ partial def equateTm (d : Q(Nat)) (l : Q(Nat)) (vT vt vu : Q(Val)) : Lean.MetaM
   | ~q(.sigma $k $k' $vA $vB) => do
     let ⟨tf, tfpost⟩ ← evalFst q($vt)
     let ⟨uf, ufpost⟩ ← evalFst q($vu)
-    let feq ← equateTm q($d) q($k) q($vA) q($tf) q($uf)
+    let feq ← equateTm q($d) q($vA) q($tf) q($uf)
     let ⟨ts, tspost⟩ ← evalSnd q($vt)
     let ⟨us, uspost⟩ ← evalSnd q($vu)
     let ⟨Btf, Btfpost⟩ ← evalClosTp q($vB) q($tf)
-    let seq ← equateTm q($d) q($k') q($Btf) q($ts) q($us)
+    let seq ← equateTm q($d) q($Btf) q($ts) q($us)
     return q(by as_aux_lemma =>
       introv deq vT vt vu
       have ⟨_, _, _, vA, vB, eq⟩ := vT.inv_sigma
@@ -151,7 +150,7 @@ partial def equateTm (d : Q(Nat)) (l : Q(Nat)) (vT vt vu : Q(Val)) : Lean.MetaM
   | ~q(.univ $k) => do
     let ⟨vA, vApost⟩ ← evalEl q($vt)
     let ⟨vA', vApost'⟩ ← evalEl q($vu)
-    let Aeq ← equateTp q($d) q($k) q($vA) q($vA')
+    let Aeq ← equateTp q($d) q($vA) q($vA')
     return q(by as_aux_lemma =>
       introv deq vT vt vu
       have ⟨_, eq⟩ := vT.inv_univ
@@ -169,13 +168,13 @@ partial def equateTm (d : Q(Nat)) (l : Q(Nat)) (vT vt vu : Q(Val)) : Lean.MetaM
     )
   | _ =>
     match vT, vt, vu with
-    | ~q(.Id $k $vA $va $vb), ~q(.refl _ _), ~q(.refl _ _) =>
+    | ~q(.Id $vA $va $vb), ~q(.refl _), ~q(.refl _) =>
       return q(by as_aux_lemma =>
         introv deq vT vt vu
-        have ⟨_, _, _, _, eqt, eq⟩ := vt.inv_refl
-        have ⟨_, _, _, _, eqt', eq'⟩ := vu.inv_refl
+        have ⟨_, _, _, eqt, eq⟩ := vt.inv_refl
+        have ⟨_, _, _, eqt', eq'⟩ := vu.inv_refl
         subst_vars
-        have ⟨_, _, _, _, _⟩ := eq.symm_tp.trans_tp eq' |>.inv_Id
+        have ⟨_, _, _⟩ := eq.symm_tp.trans_tp eq' |>.inv_Id
         apply eqt.trans_tm _ |>.trans_tm eqt'.symm_tm
         apply EqTm.conv_eq _ eq.symm_tp
         gcongr
@@ -210,14 +209,14 @@ partial def equateNeutTm (d : Q(Nat)) (nt nu : Q(Neut)) : Lean.MetaM Q(∀ {Γ T
       apply eqt.trans_tm _ |>.trans_tm (eqt'.conv_eq Aeq.symm_tp).symm_tm
       apply EqTm.refl_tm eqt.wf_right
     )
-  | ~q(.app $k _ $vA $nf $va), ~q(.app $m _ _ $nf' $va') => do
+  | ~q(.app $k $vA $nf $va), ~q(.app $m _ $nf' $va') => do
     let km ← equateNat k m
     let feq ← equateNeutTm q($d) q($nf) q($nf')
-    let aeq ← equateTm q($d) q($k) q($vA) q($va) q($va')
+    let aeq ← equateTm q($d) q($vA) q($va) q($va')
     return q(by as_aux_lemma =>
       introv _ nt nu
-      have ⟨_, _, _, _, _, vA, nf, va, eqt, eq⟩ := nt.inv_app
-      have ⟨_, _, _, _, _, vA', nf', va', eqt', eq'⟩ := nu.inv_app
+      have ⟨_, _, _, _, vA, nf, va, eqt, eq⟩ := nt.inv_app
+      have ⟨_, _, _, _, vA', nf', va', eqt', eq'⟩ := nu.inv_app
       subst_vars
       have ⟨Peq, feq⟩ := $feq rfl nf nf'
       have ⟨_, _, _, Aeq, Beq⟩ := Peq.inv_pi
@@ -262,24 +261,23 @@ partial def equateNeutTm (d : Q(Nat)) (nt nu : Q(Neut)) : Lean.MetaM Q(∀ {Γ T
         apply EqTm.conv_eq _ eq.symm_tp
         gcongr
     )
-  | ~q(.idRec $k $k' $vA $va $cM $vr $nh), ~q(.idRec $m $m' $vA' $va' $cM' $vr' $nh') => do
-    let km ← equateNat q($k) q($m)
-    let km' ← equateNat q($k') q($m')
+  | ~q(.idRec $vA $va $cM $vr $nh), ~q(.idRec $vA' $va' $cM' $vr' $nh') => do
     let heq ← equateNeutTm q($d) q($nh) q($nh')
     let ⟨Mx, Mxpost⟩ ← forceClos₂Tp
-      q($d) q($vA) q(.Id $k $vA $va (.neut (.bvar $d) $vA)) q($cM)
+      q($d) q($vA) q(.Id $vA $va (.neut (.bvar $d) $vA)) q($cM)
     let ⟨Mx', Mxpost'⟩ ← forceClos₂Tp
-      q($d) q($vA') q(.Id $k $vA' $va' (.neut (.bvar $d) $vA')) q($cM')
-    let Meq ← equateTp q($d + 2) q($k') q($Mx) q($Mx')
-    let ⟨Mrfl, Mrflpost⟩ ← evalClos₂Tp q($cM) q($va) q(.refl $k $va)
-    let req ← equateTm q($d) q($k') q($Mrfl) q($vr) q($vr')
+      q($d) q($vA') q(.Id $vA' $va' (.neut (.bvar $d) $vA')) q($cM')
+    let Meq ← equateTp q($d + 2) q($Mx) q($Mx')
+    let ⟨Mrfl, Mrflpost⟩ ← evalClos₂Tp q($cM) q($va) q(.refl $va)
+    let req ← equateTm q($d) q($Mrfl) q($vr) q($vr')
     return q(by as_aux_lemma =>
       introv _ nt nu
-      have ⟨_, _, _, _, _, _, _, vA, va, cM, vr, nh, eqt, eq⟩ := nt.inv_idRec
-      have ⟨_, _, _, _, _, _, _, vA', va', cM', vr', nh', eqt', eq'⟩ := nu.inv_idRec
+      have ⟨l, _, _, _, _, _, _, vA, va, cM, vr, nh, eqt, eq⟩ := nt.inv_idRec
+      have ⟨l', _, _, _, _, _, _, vA', va', cM', vr', nh', eqt', eq'⟩ := nu.inv_idRec
+      cases show l = l' by sorry
       subst_vars
       have ⟨eqId, heq⟩ := $heq rfl nh nh'
-      have ⟨_, _, Aeq, aeq, beq⟩ := eqId.inv_Id
+      have ⟨Aeq, aeq, beq⟩ := eqId.inv_Id
       have Mx := $Mxpost rfl vA (.Id_bvar vA va) cM
       have Mx' := $Mxpost' rfl vA' (.Id_bvar vA' va') cM'
       have Meq := by
diff --git a/GroupoidModel/Syntax/Typechecker/Evaluate.lean b/GroupoidModel/Syntax/Typechecker/Evaluate.lean
index 3f44b2bf..b5049357 100644
--- a/GroupoidModel/Syntax/Typechecker/Evaluate.lean
+++ b/GroupoidModel/Syntax/Typechecker/Evaluate.lean
@@ -8,8 +8,8 @@ open Qq
 
 theorem ValEqTp.Id_bvar {Γ vA A va a l} : ValEqTp Γ l vA A → ValEqTm Γ l va a A →
     ValEqTp ((A, l) :: Γ) l
-      (.Id l vA va (.neut (.bvar Γ.length) vA))
-      (.Id l (A.subst Expr.wk) (a.subst Expr.wk) (.bvar 0)) := by
+      (.Id vA va (.neut (.bvar Γ.length) vA))
+      (.Id (A.subst Expr.wk) (a.subst Expr.wk) (.bvar 0)) := by
   intro vA va
   have A := vA.wf_tp
   apply ValEqTp.Id (vA.wk A) (va.wk A)
@@ -50,15 +50,14 @@ partial def evalTp (env : Q(List Val)) (T' : Q(Expr)) : Lean.MetaM ((v : Q(Val))
       apply ValEqTp.sigma vAeq
       apply ClosEqTp.clos_tp env (EqTp.refl_tp vAeq.wf_tp) B
     )⟩
-  | ~q(.Id $l $A $t $u) => do
+  | ~q(.Id $A $t $u) => do
     let ⟨vA, vApost⟩ ← evalTp q($env) q($A)
     let ⟨vt, vtpost⟩ ← evalTm q($env) q($t)
     let ⟨vu, vupost⟩ ← evalTm q($env) q($u)
-    return ⟨q(.Id $l $vA $vt $vu), q(by as_aux_lemma =>
+    return ⟨q(.Id $vA $vt $vu), q(by as_aux_lemma =>
       introv env T
       simp +zetaDelta only [Expr.subst]
-      have ⟨_, t, u⟩ := T.inv_Id
-      subst_vars
+      have ⟨t, u⟩ := T.inv_Id
       apply ValEqTp.Id ($vApost env t.wf_tp) ($vtpost env t) ($vupost env u)
     )⟩
   | ~q(.el $a) => do
@@ -116,13 +115,13 @@ partial def evalTm (env : Q(List Val)) (t' : Q(Expr)) : Lean.MetaM ((v : Q(Val))
       . exact EqTp.refl_tp <| C.subst env.wf_sb
       . exact EqTp.refl_tp <| b.wf_tp.subst (env.wf_sb.up C)
     )⟩
-  | ~q(.app $k $k' $B $f $a) => do
+  | ~q(.app $k $B $f $a) => do
     let ⟨vf, vfpost⟩ ← evalTm q($env) q($f)
     let ⟨va, vapost⟩ ← evalTm q($env) q($a)
     let ⟨v, vpost⟩ ← evalApp q($vf) q($va)
     return ⟨v, q(by as_aux_lemma =>
       introv env t
-      obtain ⟨rfl, _, f, a, eq⟩ := t.inv_app
+      obtain ⟨_, f, a, eq⟩ := t.inv_app
       apply $vpost ($vfpost env f) ($vapost env a) |>.conv_tp
       convert eq.subst env.wf_sb |>.symm_tp using 1
       autosubst
@@ -158,23 +157,21 @@ partial def evalTm (env : Q(List Val)) (t' : Q(Expr)) : Lean.MetaM ((v : Q(Val))
       convert ($vpost) ($vppost env p) using 1
       autosubst
     )⟩
-  | ~q(.refl $l $u) => do
+  | ~q(.refl $u) => do
     let ⟨vu, vupost⟩ ← evalTm q($env) q($u)
-    return ⟨q(.refl $l $vu), q(by as_aux_lemma =>
+    return ⟨q(.refl $vu), q(by as_aux_lemma =>
       introv env t
-      have ⟨_, _, u, eq⟩ := t.inv_refl
-      subst_vars
+      have ⟨_, u, eq⟩ := t.inv_refl
       apply ValEqTm.conv_tp _ (eq.subst env.wf_sb).symm_tp
       apply ValEqTm.refl ($vupost env u)
     )⟩
-  | ~q(.idRec $l $l' _ $M $r _ $h) => do
+  | ~q(.idRec $l _ $M $r _ $h) => do
     let ⟨vr, vrpost⟩ ← evalTm q($env) q($r)
     let ⟨vh, vhpost⟩ ← evalTm q($env) q($h)
-    let ⟨v, vpost⟩ ← evalIdRec q($l') q(.of_expr $env $M) q($vr) q($vh)
+    let ⟨v, vpost⟩ ← evalIdRec q(.of_expr $env $M) q($vr) q($vh)
     return ⟨v, q(by as_aux_lemma =>
       introv env rec
-      have ⟨_, _, t, M, r, u, h, eq⟩ := rec.inv_idRec
-      subst_vars
+      have ⟨_, t, M, r, u, h, eq⟩ := rec.inv_idRec
       apply ValEqTm.conv_tp _ (eq.subst env.wf_sb).symm_tp
       rw [Expr.subst_snoc_toSb_subst]
       have tE := t.subst env.wf_sb
@@ -231,14 +228,13 @@ partial def evalValTp (env : Q(List Val)) (vT : Q(Val)) : Lean.MetaM ((v : Q(Val
       apply ClosEqTp.clos_val_tp env (EqTp.refl_tp vAσ.wf_tp) <|
         $vBpost env.eq_length vA vB
     )⟩
-  | ~q(.Id $k $vA $vt $vu) =>
+  | ~q(.Id $vA $vt $vu) =>
     let ⟨vA, vApost⟩ ← evalValTp q($env) q($vA)
     let ⟨vt, vtpost⟩ ← evalValTm q($env) q($vt)
     let ⟨vu, vupost⟩ ← evalValTm q($env) q($vu)
-    return ⟨q(.Id $k $vA $vt $vu), q(by as_aux_lemma =>
+    return ⟨q(.Id $vA $vt $vu), q(by as_aux_lemma =>
       introv env vT
-      have ⟨_, _, _, _, vA, vt, vu, eq⟩ := vT.inv_Id
-      subst_vars
+      have ⟨_, _, _, vA, vt, vu, eq⟩ := vT.inv_Id
       apply ValEqTp.conv_tp _ (eq.subst env.wf_sb).symm_tp
       apply ValEqTp.Id ($vApost env vA) ($vtpost env vt) ($vupost env vu)
     )⟩
@@ -295,12 +291,11 @@ partial def evalValTm (env : Q(List Val)) (vt : Q(Val)) : Lean.MetaM ((v : Q(Val
       apply ValEqTm.pair (B.subst (env.wf_sb.up B.wf_binder)) ($vfpost env vf)
       convert ($vspost env vs) using 1; autosubst
     )⟩
-  | ~q(.refl $k $va) =>
+  | ~q(.refl $va) =>
     let ⟨va, vapost⟩ ← evalValTm q($env) q($va)
-    return ⟨q(.refl $k $va), q(by as_aux_lemma =>
+    return ⟨q(.refl $va), q(by as_aux_lemma =>
       introv env vt
-      have ⟨_, _, _, va, eqt, eq⟩ := vt.inv_refl
-      subst_vars
+      have ⟨_, _, va, eqt, eq⟩ := vt.inv_refl
       apply ValEqTm.conv_tm _ (eqt.subst env.wf_sb).symm_tm
       apply ValEqTm.conv_tp _ (eq.subst env.wf_sb).symm_tp
       apply ValEqTm.refl ($vapost env va)
@@ -347,14 +342,13 @@ partial def evalNeutTm (env : Q(List Val)) (nt : Q(Neut)) : Lean.MetaM ((v : Q(V
       congr 3
       exact env.eq_length
     )⟩
-  | ~q(.app _ _ _ $nf $va) =>
+  | ~q(.app _ _ $nf $va) =>
     let ⟨vf, vfpost⟩ ← evalNeutTm q($env) q($nf)
     let ⟨va, vapost⟩ ← evalValTm q($env) q($va)
     let ⟨v, vpost⟩ ← evalApp q($vf) q($va)
     return ⟨v, q(by as_aux_lemma =>
       introv env nt
-      have ⟨_, _, _, _, _, _, nf, va, eqt, eq⟩ := nt.inv_app
-      subst_vars
+      have ⟨_, _, _, _, _, nf, va, eqt, eq⟩ := nt.inv_app
       apply ValEqTm.conv_tm _ (eqt.subst env.wf_sb).symm_tm
       apply ValEqTm.conv_tp _ (eq.subst env.wf_sb).symm_tp
       convert ($vpost ($vfpost env nf) ($vapost env va)) using 1
@@ -383,18 +377,17 @@ partial def evalNeutTm (env : Q(List Val)) (nt : Q(Neut)) : Lean.MetaM ((v : Q(V
       convert ($vpost ($vppost env np_eq)) using 1
       autosubst
     )⟩
-  | ~q(.idRec $k $k' $vA $va $cM $vr $vh) =>
+  | ~q(.idRec $vA $va $cM $vr $vh) =>
     /- NOTE: the type arguments to `forceClos₂Tp`
     are the only reason we annotate `Neut.idRec` with `vA`, `va`. -/
     let ⟨cM, cMpost⟩ ← forceClos₂Tp q(($env).length)
-      q($vA) q(.Id $k $vA $va (.neut (.bvar ($env).length) $vA)) q($cM)
+      q($vA) q(.Id $vA $va (.neut (.bvar ($env).length) $vA)) q($cM)
     let ⟨vr, vrpost⟩ ← evalValTm q($env) q($vr)
     let ⟨vh, vhpost⟩ ← evalNeutTm q($env) q($vh)
-    let ⟨v, vpost⟩ ← evalIdRec q($k') q(.of_val $env $cM) q($vr) q($vh)
+    let ⟨v, vpost⟩ ← evalIdRec q(.of_val $env $cM) q($vr) q($vh)
     return ⟨v, q(by as_aux_lemma =>
       introv env nt
       have ⟨_, _, _, _, _, _, _, vA, va, cM, vr, vh, eqt, eq⟩ := nt.inv_idRec
-      subst_vars
       apply ValEqTm.conv_tm _ (eqt.subst env.wf_sb).symm_tm
       apply ValEqTm.conv_tp _ (eq.subst env.wf_sb).symm_tp
       rw [Expr.subst_snoc_toSb_subst]
@@ -570,7 +563,7 @@ partial def evalEl (va : Q(Val)) : Lean.MetaM ((v : Q(Val)) ×
 
 partial def evalApp (vf va : Q(Val)) : Lean.MetaM ((v : Q(Val)) ×
     Q(∀ {Δ A B f a l l'}, ValEqTm Δ (max l l') $vf f (.pi l l' A B) → ValEqTm Δ l $va a A →
-      ValEqTm Δ l' $v (.app l l' B f a) (B.subst a.toSb))) :=
+      ValEqTm Δ l' $v (.app l B f a) (B.subst a.toSb))) :=
   match vf with
   | ~q(.lam $k $k' _ $vb) => do
     let ⟨v, vpost⟩ ← evalClosTm q($vb) q($va)
@@ -590,7 +583,7 @@ partial def evalApp (vf va : Q(Val)) : Lean.MetaM ((v : Q(Val)) ×
     )⟩
   | ~q(.neut $n (.pi $k $k' $vA $vB)) => do
     let ⟨vBa, vBpost⟩ ← evalClosTp q($vB) q($va)
-    return ⟨q(.neut (.app $k $k' $vA $n $va) $vBa), q(by as_aux_lemma =>
+    return ⟨q(.neut (.app $k $vA $n $va) $vBa), q(by as_aux_lemma =>
       introv vf va
       have ⟨P, n⟩ := vf.inv_neut
       have ⟨_, _, _, vA, vB, eq⟩ := P.inv_pi
@@ -674,20 +667,19 @@ partial def evalSnd (vp : Q(Val)) : Lean.MetaM ((v : Q(Val)) ×
     )⟩
   | vp => throwError "expected a normal form at type Σ, got{Lean.indentExpr vp}"
 
-partial def evalIdRec (l' : Q(Nat)) (cM : Q(Clos)) (vr vh : Q(Val)) :
-    Lean.MetaM ((v : Q(Val)) × Q(∀ {Δ A M t r u h l},
-      Clos₂EqTp Δ A l (.Id l (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0)) l $l' $cM M →
-      ValEqTm Δ $l' $vr r (M.subst (.snoc t.toSb <| .refl l t)) →
-      ValEqTm Δ l $vh h (.Id l A t u) →
-      ValEqTm Δ $l' $v (.idRec l $l' t M r u h) (M.subst (.snoc u.toSb h)))) :=
+partial def evalIdRec (cM : Q(Clos)) (vr vh : Q(Val)) :
+    Lean.MetaM ((v : Q(Val)) × Q(∀ {Δ A M t r u h l l'},
+      Clos₂EqTp Δ A l (.Id (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0)) l l' $cM M →
+      ValEqTm Δ l' $vr r (M.subst (.snoc t.toSb <| .refl t)) →
+      ValEqTm Δ l $vh h (.Id A t u) →
+      ValEqTm Δ l' $v (.idRec l t M r u h) (M.subst (.snoc u.toSb h)))) :=
   match vh with
-  | ~q(.refl $l $va) =>
+  | ~q(.refl $va) =>
     return ⟨vr, q(by as_aux_lemma =>
       introv cM vr vh
       have M := cM.wf_tp
-      have ⟨_, _, _, va, eqt, eq⟩ := vh.inv_refl
-      have ⟨_, _, _, tw, uw⟩ := eq.inv_Id
-      subst_vars
+      have ⟨_, _, va, eqt, eq⟩ := vh.inv_refl
+      have ⟨_, tw, uw⟩ := eq.inv_Id
       have tu := tw.trans_tm uw.symm_tm
       have t := tu.wf_left
       apply vr.conv_nf
@@ -700,14 +692,13 @@ partial def evalIdRec (l' : Q(Nat)) (cM : Q(Clos)) (vr vh : Q(Val)) :
         autosubst
         exact ?eq
     )⟩
-  | ~q(.neut $nh (.Id $l $vA $va $vb)) => do
+  | ~q(.neut $nh (.Id $vA $va $vb)) => do
     let ⟨vT, vTpost⟩ ← evalClos₂Tp q($cM) q($vb) q($vh)
-    return ⟨q(.neut (.idRec $l $l' $vA $va $cM $vr $nh) $vT), q(by as_aux_lemma =>
+    return ⟨q(.neut (.idRec $vA $va $cM $vr $nh) $vT), q(by as_aux_lemma =>
       introv cM vr vh
       have ⟨vId, nh⟩ := vh.inv_neut
-      have ⟨_, _, _, _, vA, va, vb, eq⟩ := vId.inv_Id
-      have ⟨_, _, _, teq, ueq⟩ := eq.inv_Id
-      subst_vars
+      have ⟨_, _, _, vA, va, vb, eq⟩ := vId.inv_Id
+      have ⟨_, teq, ueq⟩ := eq.inv_Id
       have wA := vb.wf_tm.uniq_tp ueq.wf_right
       replace vb := vb.conv_nf (ueq.symm_tm.conv_eq wA.symm_tp) wA
       have := $vTpost cM vb (autosubst% vh)
diff --git a/GroupoidModel/Syntax/Typechecker/Frontend.lean b/GroupoidModel/Syntax/Typechecker/Frontend.lean
index 8ba74197..596f1873 100644
--- a/GroupoidModel/Syntax/Typechecker/Frontend.lean
+++ b/GroupoidModel/Syntax/Typechecker/Frontend.lean
@@ -56,7 +56,7 @@ def mkSigma (l l' : Nat) : Q(_root_.Expr) :=
       .code <|
         .sigma $l $l'
           (.el <| .bvar 1)
-          (.el <| .app $l ($l' + 1) (.univ $l') (.bvar 1) (.bvar 0)))
+          (.el <| .app $l (.univ $l') (.bvar 1) (.bvar 0)))
 
 /-- Make the HoTT0 term
 `fun (A : Type l) (a b : A) : Type l => code (.Id l a b)`. -/
@@ -64,7 +64,7 @@ def mkId (l : Nat) : Q(_root_.Expr) :=
   q(.lam ($l + 1) ($l + 1) (.univ $l) <|
     .lam $l ($l + 1) (.el <| .bvar 0) <|
       .lam $l ($l + 1) (.el <| .bvar 1) <|
-        .code <| .Id $l (.el <| .bvar 2) (.bvar 1) (.bvar 0))
+        .code <| .Id (.el <| .bvar 2) (.bvar 1) (.bvar 0))
 
 mutual
 /-- Completeness: if the argument is well-formed in Lean,
@@ -134,7 +134,7 @@ partial def translateAsTm (e : Lean.Expr) : TranslateM (Nat × Q(_root_.Expr)) :
     if e.isAppOfArity' ``Id.refl 2 then
       let #[_, a] := e.getAppArgs | throwError "internal error (Id.refl)"
       let ⟨l, a⟩ ← translateAsTm a
-      return ⟨l, q(.refl $l $a)⟩
+      return ⟨l, q(.refl $a)⟩
     if e.isAppOfArity' ``Id.rec 6 then
       let #[_, a, M, r, b, h] := e.getAppArgs | throwError "internal error (Id.rec)"
       let ⟨l, a⟩ ← translateAsTm a
@@ -144,14 +144,14 @@ partial def translateAsTm (e : Lean.Expr) : TranslateM (Nat × Q(_root_.Expr)) :
       let ⟨_, r⟩ ← translateAsTm r
       let ⟨_, b⟩ ← translateAsTm b
       let ⟨_, h⟩ ← translateAsTm h
-      return ⟨l', q(.idRec $l $l' $a $M $r $b $h)⟩
+      return ⟨l', q(.idRec $l $a $M $r $b $h)⟩
     let fnTp ← inferType fn
     let ⟨_, fn⟩ ← translateAsTm fn
     let ⟨l, arg⟩ ← translateAsTm arg
     let ⟨l', B⟩ ← forallBoundedTelescope fnTp (some 1) fun xs B => do
       let #[x] := xs | throwError "internal error (app tm)"
       withBinder x <| translateAsTp B
-    return ⟨l', q(.app $l $l' $B $fn $arg)⟩
+    return ⟨l', q(.app $l $B $fn $arg)⟩
   | .const ``Sigma [l, l'] =>
     /- FIXME: To simplify the translation,
     we handle `Sigma` rather than fully applied `@Sigma α β`.
diff --git a/GroupoidModel/Syntax/Typechecker/Synth.lean b/GroupoidModel/Syntax/Typechecker/Synth.lean
index ffaf2a8b..1d61e472 100644
--- a/GroupoidModel/Syntax/Typechecker/Synth.lean
+++ b/GroupoidModel/Syntax/Typechecker/Synth.lean
@@ -54,16 +54,16 @@ partial def checkTp (vΓ : Q(TpEnv)) (l : Q(Nat)) (T : Q(Expr)) :
       subst_vars
       apply WfTp.sigma <| $Bwf <| vΓ.snoc <| $vAeq vΓ <| $Awf vΓ
     )
-  | ~q(.Id $k $A $a $b) => do
-    let leq ← equateNat q($l) q($k)
-    let Awf ← checkTp q($vΓ) q($k) q($A)
+  | ~q(.Id $A $a $b) => do
+    let Awf ← checkTp q($vΓ) q($l) q($A)
     let ⟨vA, vAeq⟩ ← evalTpId q($vΓ) q($A)
-    let awf ← checkTm q($vΓ) q($k) q($vA) q($a)
-    let bwf ← checkTm q($vΓ) q($k) q($vA) q($b)
+    let awf ← checkTm q($vΓ) q($l) q($vA) q($a)
+    let bwf ← checkTm q($vΓ) q($l) q($vA) q($b)
     return q(by as_aux_lemma =>
       introv vΓ
       subst_vars
       have := $vAeq vΓ ($Awf vΓ)
+      show Γ ⊢[«$l»] .Id $A $a $b
       apply WfTp.Id ($awf vΓ this) ($bwf vΓ this)
     )
   | ~q(.univ $n) => do
@@ -91,7 +91,7 @@ partial def checkTm (vΓ : Q(TpEnv)) (l : Q(Nat)) (vT : Q(Val)) (t : Q(Expr)) :
   /- We could do something more bidirectional,
   but all terms synthesize (thanks to extensive annotations). -/
   let ⟨vU, tU⟩ ← synthTm q($vΓ) q($l) q($t)
-  let eq ← equateTp q(($vΓ).length) q($l) q($vU) q($vT)
+  let eq ← equateTp q(($vΓ).length) q($vU) q($vT)
   return q(by as_aux_lemma =>
     introv vΓ vT
     have ⟨_, vU, t⟩ := $tU vΓ
@@ -131,11 +131,10 @@ partial def synthTm (vΓ : Q(TpEnv)) (l : Q(Nat)) (t : Q(Expr)) : Lean.MetaM ((v
       . autosubst
       . autosubst; apply EqTp.refl_tp A
     )⟩
-  | ~q(.app $k $k' $B $f $a) => do
-    let lk' ← equateNat q($l) q($k')
+  | ~q(.app $k $B $f $a) => do
     let ⟨vA, vApost⟩ ← synthTm q($vΓ) q($k) q($a)
-    let Bwf ← checkTp q(($vA, $k) :: $vΓ) q($k') q($B)
-    let fwf ← checkTm q($vΓ) q(max $k $k') q(.pi $k $k' $vA (.of_expr (envOfTpEnv $vΓ) $B)) q($f)
+    let Bwf ← checkTp q(($vA, $k) :: $vΓ) q($l) q($B)
+    let fwf ← checkTm q($vΓ) q(max $k $l) q(.pi $k $l $vA (.of_expr (envOfTpEnv $vΓ) $B)) q($f)
     let ⟨va, vaeq⟩ ← evalTmId q($vΓ) q($a)
     let ⟨vBa, vBaeq⟩ ← evalTp q($va :: envOfTpEnv $vΓ) q($B)
     return ⟨vBa, q(by as_aux_lemma =>
@@ -216,33 +215,29 @@ partial def synthTm (vΓ : Q(TpEnv)) (l : Q(Nat)) (t : Q(Expr)) : Lean.MetaM ((v
       simp +zetaDelta only [autosubst] at p ⊢
       apply WfTm.snd p
     )⟩
-  | ~q(.refl $k $a) => do
-    let leq ← equateNat q($l) q($k)
+  | ~q(.refl $a) => do
     let ⟨vA, vApost⟩ ← synthTm q($vΓ) q($l) q($a)
     let ⟨va, vapost⟩ ← evalTmId q($vΓ) q($a)
-    return ⟨q(.Id $k $vA $va $va), q(by as_aux_lemma =>
+    return ⟨q(.Id $vA $va $va), q(by as_aux_lemma =>
       introv vΓ
-      subst_vars
       have ⟨_, vA, a⟩ := $vApost vΓ
       have va := $vapost vΓ a
       refine ⟨_, ValEqTp.Id vA va va, WfTm.refl a⟩
     )⟩
-  | ~q(.idRec $k $k' $a $M $r $b $h) => do
-    let leq ← equateNat q($l) q($k')
+  | ~q(.idRec $k $a $M $r $b $h) => do
     let ⟨vA, vApost⟩ ← synthTm q($vΓ) q($k) q($a)
     let ⟨va, vapost⟩ ← evalTmId q($vΓ) q($a)
     let Mwf ← checkTp
-      q((.Id $k $vA $va (.neut (.bvar ($vΓ).length) $vA), $k) :: ($vA, $k) :: $vΓ) q($k') q($M)
-    let ⟨vMa, vMapost⟩ ← evalTp q((.refl $k $va) :: $va :: envOfTpEnv $vΓ) q($M)
-    let rwf ← checkTm q($vΓ) q($k') q($vMa) q($r)
+      q((.Id $vA $va (.neut (.bvar ($vΓ).length) $vA), $k) :: ($vA, $k) :: $vΓ) q($l) q($M)
+    let ⟨vMa, vMapost⟩ ← evalTp q((.refl $va) :: $va :: envOfTpEnv $vΓ) q($M)
+    let rwf ← checkTm q($vΓ) q($l) q($vMa) q($r)
     let bwf ← checkTm q($vΓ) q($k) q($vA) q($b)
     let ⟨vb, vbpost⟩ ← evalTmId q($vΓ) q($b)
-    let hwf ← checkTm q($vΓ) q($k) q(.Id $k $vA $va $vb) q($h)
+    let hwf ← checkTm q($vΓ) q($k) q(.Id $vA $va $vb) q($h)
     let ⟨vh, vhpost⟩ ← evalTmId q($vΓ) q($h)
     let ⟨vMb, vMbpost⟩ ← evalTp q($vh :: $vb :: envOfTpEnv $vΓ) q($M)
     return ⟨q($vMb), q(by as_aux_lemma =>
       introv vΓ
-      subst_vars
       have ⟨_, vA, a⟩ := $vApost vΓ
       have va := $vapost vΓ a
       have := ValEqTp.Id_bvar vA va
diff --git a/GroupoidModel/Syntax/Typechecker/Value.lean b/GroupoidModel/Syntax/Typechecker/Value.lean
index e0b85c16..ef8eeede 100644
--- a/GroupoidModel/Syntax/Typechecker/Value.lean
+++ b/GroupoidModel/Syntax/Typechecker/Value.lean
@@ -44,7 +44,7 @@ and hence it suffices to compare the value parts (in this case `p`). -/
 inductive Val where
   | pi (l l' : Nat) (A : Val) (B : Clos)
   | sigma (l l' : Nat) (A : Val) (B : Clos)
-  | Id (l : Nat) (A t u : Val)
+  | Id (A t u : Val)
   | univ (l : Nat)
   /-- Although `el` is an eliminator,
   as a neutral form it does not need to be annotated with a type
@@ -53,7 +53,7 @@ inductive Val where
   | el (a : Neut)
   | lam (l l' : Nat) (vA : Val) (b : Clos)
   | pair (l l' : Nat) (t u : Val)
-  | refl (l : Nat) (t : Val)
+  | refl (t : Val)
   | code (A : Val)
   /-- A neutral form at the given type. -/
   | neut (n : Neut) (A : Val)
@@ -65,10 +65,10 @@ inductive Neut where
   /-- A de Bruijn *level*. -/
   | bvar (i : Nat)
   /-- Application at the specified argument type. -/
-  | app (l l' : Nat) (A : Val) (f : Neut) (a : Val)
+  | app (l : Nat) (A : Val) (f : Neut) (a : Val)
   | fst (l l' : Nat) (p : Neut)
   | snd (l l' : Nat) (p : Neut)
-  | idRec (l l' : Nat) (A a : Val) (M : Clos) (r : Val) (h : Neut)
+  | idRec (A a : Val) (M : Clos) (r : Val) (h : Neut)
   deriving Inhabited
 
 /-- Recall that given `Γ.A ⊢ b : B` and a substitution `Δ ⊢ env : Γ`,
@@ -104,7 +104,7 @@ inductive ValEqTp : Ctx → Nat → Val → Expr → Prop
     ValEqTp Γ l vA A →
     ValEqTm Γ l vt t A →
     ValEqTm Γ l vu u A →
-    ValEqTp Γ l (.Id l vA vt vu) (.Id l A t u)
+    ValEqTp Γ l (.Id vA vt vu) (.Id A t u)
   | univ {Γ l} :
     WfCtx Γ →
     l < univMax →
@@ -131,7 +131,7 @@ inductive ValEqTm : Ctx → Nat → Val → Expr → Expr → Prop
     ValEqTm Γ (max l l') (.pair l l' vt vu) (.pair l l' B t u) (.sigma l l' A B)
   | refl {Γ A vt t l} :
     ValEqTm Γ l vt t A →
-    ValEqTm Γ l (.refl l vt) (.refl l t) (.Id l A t t)
+    ValEqTm Γ l (.refl vt) (.refl t) (.Id A t t)
   | code {Γ vA A l} :
     l < univMax →
     ValEqTp Γ l vA A →
@@ -155,7 +155,7 @@ inductive NeutEqTm : Ctx → Nat → Neut → Expr → Expr → Prop
     ValEqTp Γ l vA A →
     NeutEqTm Γ (max l l') vf f (.pi l l' A B) →
     ValEqTm Γ l va a A →
-    NeutEqTm Γ l' (.app l l' vA vf va) (.app l l' B f a) (B.subst a.toSb)
+    NeutEqTm Γ l' (.app l vA vf va) (.app l B f a) (B.subst a.toSb)
   | fst {Γ A B vp p l l'} :
     NeutEqTm Γ (max l l') vp p (.sigma l l' A B) →
     NeutEqTm Γ l (.fst l l' vp) (.fst l l' A B p) A
@@ -165,10 +165,10 @@ inductive NeutEqTm : Ctx → Nat → Neut → Expr → Expr → Prop
   | idRec {Γ vA A cM M va a vr r b nh h l l'} :
     ValEqTp Γ l vA A →
     ValEqTm Γ l va a A →
-    Clos₂EqTp Γ A l (.Id l (A.subst Expr.wk) (a.subst Expr.wk) (.bvar 0)) l l' cM M →
-    ValEqTm Γ l' vr r (M.subst (.snoc a.toSb <| .refl l a)) →
-    NeutEqTm Γ l nh h (.Id l A a b) →
-    NeutEqTm Γ l' (.idRec l l' vA va cM vr nh) (.idRec l l' a M r b h) (M.subst (.snoc b.toSb h))
+    Clos₂EqTp Γ A l (.Id (A.subst Expr.wk) (a.subst Expr.wk) (.bvar 0)) l l' cM M →
+    ValEqTm Γ l' vr r (M.subst (.snoc a.toSb <| .refl a)) →
+    NeutEqTm Γ l nh h (.Id A a b) →
+    NeutEqTm Γ l' (.idRec vA va cM vr nh) (.idRec l a M r b h) (M.subst (.snoc b.toSb h))
   | conv_neut {Γ A A' vn n n' l} :
     NeutEqTm Γ l vn n A →
     Γ ⊢[l] n ≡ n' : A →
@@ -667,14 +667,14 @@ theorem ValEqTp.inv_sigma {Γ C vA vB l k k'} : ValEqTp Γ l (.sigma k k' vA vB)
   mutual_induction ValEqTp
   all_goals grind [WfTp.sigma, ClosEqTp.wf_tp]
 
-theorem ValEqTp.inv_Id {Γ C vA vt vu l k} : ValEqTp Γ l (.Id k vA vt vu) C →
-    l = k ∧ ∃ A t u,
-      ValEqTp Γ k vA A ∧ ValEqTm Γ k vt t A ∧ ValEqTm Γ k vu u A ∧
-      (Γ ⊢[k] C ≡ .Id k A t u) := by
+theorem ValEqTp.inv_Id {Γ C vA vt vu l} : ValEqTp Γ l (.Id vA vt vu) C →
+    ∃ A t u,
+      ValEqTp Γ l vA A ∧ ValEqTm Γ l vt t A ∧ ValEqTm Γ l vu u A ∧
+      (Γ ⊢[l] C ≡ .Id A t u) := by
   suffices ∀ {Γ l vC C}, ValEqTp Γ l vC C →
-    ∀ {vA vt vu k}, vC = .Id k vA vt vu →
-    l = k ∧ ∃ A t u, ValEqTp Γ k vA A ∧ ValEqTm Γ k vt t A ∧ ValEqTm Γ k vu u A ∧
-      (Γ ⊢[k] C ≡ .Id k A t u) from
+    ∀ {vA vt vu}, vC = .Id vA vt vu →
+    ∃ A t u, ValEqTp Γ l vA A ∧ ValEqTm Γ l vt t A ∧ ValEqTm Γ l vu u A ∧
+      (Γ ⊢[l] C ≡ .Id A t u) from
   fun h => this h rfl
   mutual_induction ValEqTp
   case Id =>
@@ -738,11 +738,11 @@ theorem ValEqTm.inv_pair {Γ C vt vu p l₀ l l'} : ValEqTm Γ l₀ (.pair l l'
   case conv_nf => grind [EqTm.conv_eq]
   case pair => grind [WfTm.pair, ValEqTm.wf_tm, WfTp.sigma]
 
-theorem ValEqTm.inv_refl {Γ C vt r l₀ l} : ValEqTm Γ l₀ (.refl l vt) r C →
-    l₀ = l ∧ ∃ A t, (ValEqTm Γ l vt t A) ∧
-      (Γ ⊢[l] r ≡ .refl l t : C) ∧ (Γ ⊢[l] C ≡ .Id l A t t) := by
-  suffices ∀ {Γ l₀ vr r C}, ValEqTm Γ l₀ vr r C → ∀ {vt l}, vr = .refl l vt → l₀ = l ∧ ∃ A t,
-      (ValEqTm Γ l vt t A) ∧ (Γ ⊢[l] r ≡ .refl l t : C) ∧ (Γ ⊢[l] C ≡ .Id l A t t) from
+theorem ValEqTm.inv_refl {Γ C vt r l} : ValEqTm Γ l (.refl vt) r C →
+    ∃ A t, (ValEqTm Γ l vt t A) ∧
+      (Γ ⊢[l] r ≡ .refl t : C) ∧ (Γ ⊢[l] C ≡ .Id A t t) := by
+  suffices ∀ {Γ l vr r C}, ValEqTm Γ l vr r C → ∀ {vt}, vr = .refl vt → ∃ A t,
+      (ValEqTm Γ l vt t A) ∧ (Γ ⊢[l] r ≡ .refl t : C) ∧ (Γ ⊢[l] C ≡ .Id A t t) from
     fun h => this h rfl
   mutual_induction ValEqTm
   case refl =>
@@ -751,24 +751,24 @@ theorem ValEqTm.inv_refl {Γ C vt r l₀ l} : ValEqTm Γ l₀ (.refl l vt) r C 
     grind [WfTm.refl, WfTp.Id]
   all_goals grind [EqTm.conv_eq]
 
-theorem NeutEqTm.inv_idRec {Γ C vA cM va vr nh j l₀ l l'} :
-    NeutEqTm Γ l₀ (.idRec l l' vA va cM vr nh) j C → l₀ = l' ∧ ∃ A M t r u h,
+theorem NeutEqTm.inv_idRec {Γ C vA cM va vr nh j l'} :
+    NeutEqTm Γ l' (.idRec vA va cM vr nh) j C → ∃ l A M t r u h,
       (ValEqTp Γ l vA A) ∧
       (ValEqTm Γ l va t A) ∧
-      (Clos₂EqTp Γ A l (.Id l (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0)) l l' cM M) ∧
-      (ValEqTm Γ l' vr r (M.subst (.snoc t.toSb <| .refl l t))) ∧
-      (NeutEqTm Γ l nh h (.Id l A t u)) ∧
-      (Γ ⊢[l'] j ≡ .idRec l l' t M r u h : C) ∧
+      (Clos₂EqTp Γ A l (.Id (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0)) l l' cM M) ∧
+      (ValEqTm Γ l' vr r (M.subst (.snoc t.toSb <| .refl t))) ∧
+      (NeutEqTm Γ l nh h (.Id A t u)) ∧
+      (Γ ⊢[l'] j ≡ .idRec l t M r u h : C) ∧
       (Γ ⊢[l'] C ≡ M.subst (.snoc u.toSb h)) := by
   suffices
-    ∀ {Γ l₀ vj j C}, NeutEqTm Γ l₀ vj j C → ∀ {vA cM va vr nh l l'},
-      vj = .idRec l l' vA va cM vr nh → l₀ = l' ∧ ∃ A M t r u h,
+    ∀ {Γ l' vj j C}, NeutEqTm Γ l' vj j C → ∀ {vA cM va vr nh},
+      vj = .idRec vA va cM vr nh → ∃ l A M t r u h,
         (ValEqTp Γ l vA A) ∧
         (ValEqTm Γ l va t A) ∧
-        (Clos₂EqTp Γ A l (.Id l (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0)) l l' cM M) ∧
-        (ValEqTm Γ l' vr r (M.subst (.snoc t.toSb <| .refl l t))) ∧
-        (NeutEqTm Γ l nh h (.Id l A t u)) ∧
-        (Γ ⊢[l'] j ≡ .idRec l l' t M r u h : C) ∧
+        (Clos₂EqTp Γ A l (.Id (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0)) l l' cM M) ∧
+        (ValEqTm Γ l' vr r (M.subst (.snoc t.toSb <| .refl t))) ∧
+        (NeutEqTm Γ l nh h (.Id A t u)) ∧
+        (Γ ⊢[l'] j ≡ .idRec l t M r u h : C) ∧
         (Γ ⊢[l'] C ≡ M.subst (.snoc u.toSb h)) from
     fun h => this h rfl
   mutual_induction ValEqTm
@@ -813,14 +813,14 @@ theorem NeutEqTm.inv_bvar {Γ A t i l} : NeutEqTm Γ l (.bvar i) t A →
     exact ⟨_, lk, EqTm.refl_tm (WfTm.bvar (by omega) lk), EqTp.refl_tp (Γwf.lookup_wf lk)⟩
   case conv_neut => grind [EqTm.conv_eq]
 
-theorem NeutEqTm.inv_app {Γ vA C vf va t l₀ l l'} : NeutEqTm Γ l₀ (.app l l' vA vf va) t C →
-    l₀ = l' ∧ ∃ A B f a,
+theorem NeutEqTm.inv_app {Γ vA C vf va t l l'} : NeutEqTm Γ l' (.app l vA vf va) t C →
+    ∃ A B f a,
       ValEqTp Γ l vA A ∧ NeutEqTm Γ (max l l') vf f (.pi l l' A B) ∧ ValEqTm Γ l va a A ∧
-      (Γ ⊢[l'] t ≡ .app l l' B f a : C) ∧ (Γ ⊢[l'] C ≡ B.subst a.toSb) := by
-  suffices ∀ {Γ l₀ vn n C}, NeutEqTm Γ l₀ vn n C → ∀ {vA vf va l l'}, vn = .app l l' vA vf va →
-      l₀ = l' ∧ ∃ A B f a,
+      (Γ ⊢[l'] t ≡ .app l B f a : C) ∧ (Γ ⊢[l'] C ≡ B.subst a.toSb) := by
+  suffices ∀ {Γ l' vn n C}, NeutEqTm Γ l' vn n C → ∀ {vA vf va l}, vn = .app l vA vf va →
+      ∃ A B f a,
         ValEqTp Γ l vA A ∧ NeutEqTm Γ (max l l') vf f (.pi l l' A B) ∧ ValEqTm Γ l va a A ∧
-        (Γ ⊢[l'] n ≡ .app l l' B f a : C) ∧ (Γ ⊢[l'] C ≡ B.subst a.toSb) from
+        (Γ ⊢[l'] n ≡ .app l B f a : C) ∧ (Γ ⊢[l'] C ≡ B.subst a.toSb) from
     fun h => this h rfl
   mutual_induction NeutEqTm
   all_goals intros; try exact True.intro
diff --git a/GroupoidModel/Syntax/Typing.lean b/GroupoidModel/Syntax/Typing.lean
index c227bb01..cfa1a96b 100644
--- a/GroupoidModel/Syntax/Typing.lean
+++ b/GroupoidModel/Syntax/Typing.lean
@@ -79,7 +79,7 @@ inductive WfTp : Ctx → Nat → Expr → Prop
     Γ ⊢[l] A →
     Γ ⊢[l] t : A →
     Γ ⊢[l] u : A →
-    Γ ⊢[l] .Id l A t u
+    Γ ⊢[l] .Id A t u
 
   | univ {Γ l} :
     WfCtx Γ →
@@ -111,7 +111,7 @@ inductive EqTp : Ctx → Nat → Expr → Expr → Prop
     Γ ⊢[l] A ≡ A' →
     Γ ⊢[l] t ≡ t' : A →
     Γ ⊢[l] u ≡ u' : A →
-    Γ ⊢[l] .Id l A t u ≡ .Id l A' t' u'
+    Γ ⊢[l] .Id A t u ≡ .Id A' t' u'
 
   | cong_el {Γ A A' l} :
     Γ ⊢[l+1] A ≡ A' : .univ l →
@@ -157,7 +157,7 @@ inductive WfTm : Ctx → Nat → Expr → Expr → Prop
     (A,l) :: Γ ⊢[l'] B →
     Γ ⊢[max l l'] f : .pi l l' A B →
     Γ ⊢[l] a : A →
-    Γ ⊢[l'] .app l l' B f a : B.subst a.toSb
+    Γ ⊢[l'] .app l B f a : B.subst a.toSb
 
   | pair' {Γ A B t u l l'} :
     Γ ⊢[l] A →
@@ -181,16 +181,16 @@ inductive WfTm : Ctx → Nat → Expr → Expr → Prop
   | refl' {Γ A t l} :
     Γ ⊢[l] A →
     Γ ⊢[l] t : A →
-    Γ ⊢[l] .refl l t : .Id l A t t
+    Γ ⊢[l] .refl t : .Id A t t
 
   | idRec' {Γ A M t r u h l l'} :
     Γ ⊢[l] A →
     Γ ⊢[l] t : A →
-    (.Id l (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M →
-    Γ ⊢[l'] r : M.subst (.snoc t.toSb <| .refl l t) →
+    (.Id (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M →
+    Γ ⊢[l'] r : M.subst (.snoc t.toSb <| .refl t) →
     Γ ⊢[l] u : A →
-    Γ ⊢[l] h : .Id l A t u →
-    Γ ⊢[l'] .idRec l l' t M r u h : M.subst (.snoc u.toSb h)
+    Γ ⊢[l] h : .Id A t u →
+    Γ ⊢[l'] .idRec l t M r u h : M.subst (.snoc u.toSb h)
 
   | code {Γ A l} :
     l < univMax →
@@ -221,7 +221,7 @@ inductive EqTm : Ctx → Nat → Expr → Expr → Expr → Prop
     (A,l) :: Γ ⊢[l'] B ≡ B' →
     Γ ⊢[max l l'] f ≡ f' : .pi l l' A B →
     Γ ⊢[l] a ≡ a' : A →
-    Γ ⊢[l'] .app l l' B f a ≡ .app l l' B' f' a' : B.subst a.toSb
+    Γ ⊢[l'] .app l B f a ≡ .app l B' f' a' : B.subst a.toSb
 
   | cong_pair' {Γ A B B' t t' u u' l l'} :
     Γ ⊢[l] A →
@@ -247,17 +247,17 @@ inductive EqTm : Ctx → Nat → Expr → Expr → Expr → Prop
   | cong_refl' {Γ A t t' l} :
     Γ ⊢[l] A →
     Γ ⊢[l] t ≡ t' : A →
-    Γ ⊢[l] .refl l t ≡ .refl l t' : .Id l A t t
+    Γ ⊢[l] .refl t ≡ .refl t' : .Id A t t
 
   | cong_idRec' {Γ A M M' t t' r r' u u' h h' l l'} :
     Γ ⊢[l] A →
     Γ ⊢[l] t : A →
     Γ ⊢[l] t ≡ t' : A →
-    (.Id l (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M ≡ M' →
-    Γ ⊢[l'] r ≡ r' : M.subst (.snoc t.toSb <| .refl l t) →
+    (.Id (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M ≡ M' →
+    Γ ⊢[l'] r ≡ r' : M.subst (.snoc t.toSb <| .refl t) →
     Γ ⊢[l] u ≡ u' : A →
-    Γ ⊢[l] h ≡ h' : .Id l A t u →
-    Γ ⊢[l'] .idRec l l' t M r u h ≡ .idRec l l' t' M' r' u' h' : M.subst (.snoc u.toSb h)
+    Γ ⊢[l] h ≡ h' : .Id A t u →
+    Γ ⊢[l'] .idRec l t M r u h ≡ .idRec l t' M' r' u' h' : M.subst (.snoc u.toSb h)
 
   | cong_code {Γ A A' l} :
     l < univMax →
@@ -270,7 +270,7 @@ inductive EqTm : Ctx → Nat → Expr → Expr → Expr → Prop
     (A,l) :: Γ ⊢[l'] B →
     (A,l) :: Γ ⊢[l'] t : B →
     Γ ⊢[l] u : A →
-    Γ ⊢[l'] .app l l' B (.lam l l' A t) u ≡ t.subst u.toSb : B.subst u.toSb
+    Γ ⊢[l'] .app l B (.lam l l' A t) u ≡ t.subst u.toSb : B.subst u.toSb
 
   | fst_pair' {Γ} {A B t u : Expr} {l l'} :
     Γ ⊢[l] A →
@@ -289,9 +289,9 @@ inductive EqTm : Ctx → Nat → Expr → Expr → Expr → Prop
   | idRec_refl' {Γ A M t r l l'} :
     Γ ⊢[l] A →
     Γ ⊢[l] t : A →
-    (.Id l (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M →
-    Γ ⊢[l'] r : M.subst (.snoc t.toSb <| .refl l t) →
-    Γ ⊢[l'] .idRec l l' t M r t (.refl l t) ≡ r : M.subst (.snoc t.toSb <| .refl l t)
+    (.Id (A.subst Expr.wk) (t.subst Expr.wk) (.bvar 0), l) :: (A, l) :: Γ ⊢[l'] M →
+    Γ ⊢[l'] r : M.subst (.snoc t.toSb <| .refl t) →
+    Γ ⊢[l'] .idRec l t M r t (.refl t) ≡ r : M.subst (.snoc t.toSb <| .refl t)
 
   -- Expansions
   | lam_app' {Γ A B f l l'} :
@@ -299,7 +299,7 @@ inductive EqTm : Ctx → Nat → Expr → Expr → Expr → Prop
     (A,l) :: Γ ⊢[l'] B →
     Γ ⊢[max l l'] f : .pi l l' A B →
     Γ ⊢[max l l'] f ≡
-      .lam l l' A (.app l l' (B.subst (Expr.up Expr.wk)) (f.subst Expr.wk) (.bvar 0)) :
+      .lam l l' A (.app l (B.subst (Expr.up Expr.wk)) (f.subst Expr.wk) (.bvar 0)) :
       .pi l l' A B
 
   | pair_fst_snd' {Γ A B p l l'} :