From 0ddd4a88b2706971f3b27ba13e19ec972d65b581 Mon Sep 17 00:00:00 2001
From: Matt Hunzinger <matt@hunzinger.me>
Date: Mon, 2 Mar 2026 23:07:53 -0500
Subject: [PATCH 01/17] feat: Term

---
 .../LambdaCalculus/Named/Coc/Basic.lean       | 44 +++++++++++++++++++
 references.bib                                | 14 ++++++
 2 files changed, 58 insertions(+)
 create mode 100644 Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean

diff --git a/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean b/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean
new file mode 100644
index 000000000..1619cc030
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean
@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2026 Matt Hunzinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Matt Hunzinger
+-/
+
+module
+
+public import Cslib.Foundations.Data.HasFresh
+public import Cslib.Foundations.Syntax.HasAlphaEquiv
+public import Cslib.Foundations.Syntax.HasSubstitution
+
+@[expose] public section
+
+/-! # Calculus of Constructions
+
+The Calculus of Constructions
+
+## References
+
+* [T. Coquand, *An algorithm for type-checking dependent types*][Coquand1996]
+
+-/
+
+namespace Cslib
+
+universe u
+
+variable {Var : Type u}
+
+namespace LambdaCalculus.Named.Coc
+
+/-- Syntax of terms. -/
+inductive Term (Var : Type u) : Type u
+  | var : Var → Term Var
+  | app : Term Var → Term Var → Term Var
+  | lam : Var → Term Var → Term Var → Term Var
+  | pi : Var → Term Var → Term Var → Term Var
+  | type : Term Var
+deriving DecidableEq
+
+end LambdaCalculus.Named.Coc
+
+end Cslib
diff --git a/references.bib b/references.bib
index 3ad80fe85..5999a7c8b 100644
--- a/references.bib
+++ b/references.bib
@@ -28,6 +28,20 @@ @book{Baader1998
 address = {USA}
 }
 
+@article{Coquand1996,
+title = {An algorithm for type-checking dependent types},
+journal = {Science of Computer Programming},
+volume = {26},
+number = {1},
+pages = {167-177},
+year = {1996},
+issn = {0167-6423},
+doi = {https://doi.org/10.1016/0167-6423(95)00021-6},
+url = {https://www.sciencedirect.com/science/article/pii/0167642395000216},
+author = {Thierry Coquand},
+abstract = {We present a simple type-checker for a language with dependent types and let expressions, with a simple proof of correctness.}
+}
+
 @inproceedings{Danielsson2008,
 author = {Danielsson, Nils Anders},
 title = {Lightweight semiformal time complexity analysis for purely functional data structures},

From 448207e1f49452d6cea9ff4a310db6348f787f99 Mon Sep 17 00:00:00 2001
From: Matt Hunzinger <matt@hunzinger.me>
Date: Tue, 3 Mar 2026 00:02:20 -0500
Subject: [PATCH 02/17] feat: Term.rename

---
 .../LambdaCalculus/Named/Coc/Basic.lean         | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean b/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean
index 1619cc030..d583a9c50 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean
@@ -39,6 +39,23 @@ inductive Term (Var : Type u) : Type u
   | type : Term Var
 deriving DecidableEq
 
+namespace Term
+
+/-- Renaming, or variable substitution. `m.rename x y` renames `x` into `y` in `m`. -/
+def rename [DecidableEq Var] (m : Term Var) (x : Var) (y : Var) : Term Var := match m with
+  | .var z => if z = x then .var y else .var z
+  | .app f a => .app (f.rename x y) (a.rename x y)
+  | .lam v t b => .lam v (t.rename x y) (b.rename x y)
+  | .pi v t b => .pi v (t.rename x y) (b.rename x y)
+  | .type => .type
+
+/-- Renaming preserves size. -/
+theorem rename.eq_sizeOf {m : Term Var} {x y : Var} [DecidableEq Var] :
+    sizeOf (m.rename x y) = sizeOf m := by
+  induction m <;> simp_all [Term.rename] ; split <;> simp_all
+
+end Term
+
 end LambdaCalculus.Named.Coc
 
 end Cslib

From 745a7c62db9d818e567ca002f7b593f63d9aa0cc Mon Sep 17 00:00:00 2001
From: Matt Hunzinger <matt@hunzinger.me>
Date: Tue, 3 Mar 2026 00:07:34 -0500
Subject: [PATCH 03/17] feat: Term.subst

---
 .../LambdaCalculus/Named/Coc/Basic.lean       | 52 +++++++++++++++++++
 1 file changed, 52 insertions(+)

diff --git a/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean b/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean
index d583a9c50..8d63e4e7e 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean
@@ -54,6 +54,58 @@ theorem rename.eq_sizeOf {m : Term Var} {x y : Var} [DecidableEq Var] :
     sizeOf (m.rename x y) = sizeOf m := by
   induction m <;> simp_all [Term.rename] ; split <;> simp_all
 
+/-- Free variables. -/
+def fv [DecidableEq Var] : Term Var → Finset Var
+  | .var z => {z}
+  | .app f a => f.fv ∪ a.fv
+  | .lam v t b => (t.fv ∪ b.fv).erase v
+  | .pi v t b => (t.fv ∪ b.fv).erase v
+  | .type => ∅
+
+/-- Bound variables. -/
+def bv [DecidableEq Var] : Term Var → Finset Var
+  | .var _ => ∅
+  | .app f a => f.bv ∪ a.bv
+  | .lam v t b => (t.bv ∪ b.bv) ∪ {v}
+  | .pi v t b => (t.bv ∪ b.bv) ∪ {v}
+  | .type => ∅
+
+/-- Variable names (free and bound) in a term. -/
+def vars [DecidableEq Var] (t : Term Var) : Finset Var := t.fv ∪ t.bv
+
+/--
+Capture-avoiding substitution.
+`m.subst x r` replaces the free occurrences of variable `x` in `m` with `r`.
+-/
+def subst [DecidableEq Var] [HasFresh Var] (m : Term Var) (x : Var) (r : Term Var) : Term Var :=
+  match m with
+  | .var z => if z = x then r else .var z
+  | .app f a => .app (f.subst x r) (a.subst x r)
+  | .lam y t b =>
+    if y = x then
+      .lam y (t.subst x r) b
+    else if y ∉ r.fv then
+      .lam y (t.subst x r) (b.subst x r)
+    else
+      let z := HasFresh.fresh (t.vars ∪ b.vars ∪ r.vars ∪ {y})
+      .lam z ((t.rename y z).subst x r) ((b.rename y z).subst x r)
+  | .pi y t b =>
+    if y = x then
+      .pi y (t.subst x r) b
+    else if y ∉ r.fv then
+      .pi y (t.subst x r) (b.subst x r)
+    else
+      let z := HasFresh.fresh (t.vars ∪ b.vars ∪ r.vars ∪ {y})
+      .pi z ((t.rename y z).subst x r) ((b.rename y z).subst x r)
+  | .type => .type
+  termination_by m
+  decreasing_by all_goals grind [rename.eq_sizeOf]
+
+/-- `Term.subst` is a substitution for λ-terms. Gives access to the notation `m[x := n]`. -/
+instance instHasSubstitutionTerm [DecidableEq Var] [HasFresh Var] :
+    HasSubstitution (Term Var) Var (Term Var) where
+  subst := Term.subst
+
 end Term
 
 end LambdaCalculus.Named.Coc

From 1d265e4a82a0f67b1c58feb1683e299e5a41c749 Mon Sep 17 00:00:00 2001
From: Matt Hunzinger <matt@hunzinger.me>
Date: Tue, 3 Mar 2026 00:15:10 -0500
Subject: [PATCH 04/17] feat: Term.BetaEquiv and HasBetaEquiv

---
 Cslib/Foundations/Syntax/HasBetaEquiv.lean    | 23 +++++++++++++++++++
 .../LambdaCalculus/Named/Coc/Basic.lean       | 11 +++++++++
 2 files changed, 34 insertions(+)
 create mode 100644 Cslib/Foundations/Syntax/HasBetaEquiv.lean

diff --git a/Cslib/Foundations/Syntax/HasBetaEquiv.lean b/Cslib/Foundations/Syntax/HasBetaEquiv.lean
new file mode 100644
index 000000000..e35f7ec01
--- /dev/null
+++ b/Cslib/Foundations/Syntax/HasBetaEquiv.lean
@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2026 Matt Hunzinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Matt Hunzinger
+-/
+
+module
+
+public import Cslib.Init
+
+public section
+
+namespace Cslib
+
+/-- Typeclass for the β-equivalence notation `x =β y`. -/
+class HasBetaEquiv (β : Type u) where
+  /-- β-equivalence relation for type β. -/
+  BetaEquiv : β → β → Prop
+
+@[inherit_doc]
+notation m:max " =β " n:max => HasBetaEquiv.BetaEquiv m n
+
+end Cslib
diff --git a/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean b/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean
index 8d63e4e7e..a70a40471 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean
@@ -8,6 +8,7 @@ module
 
 public import Cslib.Foundations.Data.HasFresh
 public import Cslib.Foundations.Syntax.HasAlphaEquiv
+public import Cslib.Foundations.Syntax.HasBetaEquiv
 public import Cslib.Foundations.Syntax.HasSubstitution
 
 @[expose] public section
@@ -106,6 +107,16 @@ instance instHasSubstitutionTerm [DecidableEq Var] [HasFresh Var] :
     HasSubstitution (Term Var) Var (Term Var) where
   subst := Term.subst
 
+/-- β-equivalence. -/
+inductive BetaEquiv [DecidableEq Var] [HasFresh Var] : Term Var → Term Var → Prop
+  /-- Equivalance -/
+  | eq : BetaEquiv (B [x := N]) (.app (.lam x A B) N)
+  /-- Congruence -/
+  | cong : BetaEquiv B A → BetaEquiv N M → BetaEquiv (.app B N) (.app A M)
+
+instance instHasBetaEquivTerm [DecidableEq Var] [HasFresh Var] : HasBetaEquiv (Term Var) where
+  BetaEquiv := BetaEquiv
+
 end Term
 
 end LambdaCalculus.Named.Coc

From 7979775b32b5668ad66104de863c5f98e13f4523 Mon Sep 17 00:00:00 2001
From: Matt Hunzinger <matt@hunzinger.me>
Date: Tue, 3 Mar 2026 00:37:09 -0500
Subject: [PATCH 05/17] feat: Typing

---
 .../Languages/LambdaCalculus/Named/Coc/Basic.lean | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean b/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean
index a70a40471..2c0933a77 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean
@@ -117,6 +117,21 @@ inductive BetaEquiv [DecidableEq Var] [HasFresh Var] : Term Var → Term Var →
 instance instHasBetaEquivTerm [DecidableEq Var] [HasFresh Var] : HasBetaEquiv (Term Var) where
   BetaEquiv := BetaEquiv
 
+/-- Typing judgement -/
+inductive Typing [DecidableEq v] [HasFresh v] : List (v × Term v) → Term v → Term v → Prop
+  /-- Variable lookup in Γ -/
+  | var : ⟨x, A⟩ ∈ Γ → Typing Γ (.var x) A
+  /-- Function application -/
+  | app : Typing Γ M (.pi x A B) → Typing Γ N A → Typing Γ (.app M N) (B[x := N])
+  /-- Lambda -/
+  | lam : Typing Γ A K → Typing (⟨x, A⟩ :: Γ) N B → Typing Γ (.lam x A N) (.pi x A B)
+  /-- Pi -/
+  | pi : Typing Γ A K → Typing (⟨x, A⟩ :: Γ) B L → Typing Γ (.pi x A B) L
+  /-- Type -/
+  | type : Typing Γ .type .type
+  /-- Conversion -/
+  | conv : Typing Γ M A → A =β B → Typing Γ M B
+
 end Term
 
 end LambdaCalculus.Named.Coc

From e8cef246acd56156f9acc77ef9a3831d7d4567b1 Mon Sep 17 00:00:00 2001
From: Matt Hunzinger <matt@hunzinger.me>
Date: Tue, 3 Mar 2026 11:42:15 -0500
Subject: [PATCH 06/17] refactor: rename lam to abs to fit styling of other AST

---
 Cslib/Foundations/Syntax/HasBetaEquiv.lean    |  6 +++---
 .../LambdaCalculus/Named/Coc/Basic.lean       | 20 +++++++++----------
 2 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/Cslib/Foundations/Syntax/HasBetaEquiv.lean b/Cslib/Foundations/Syntax/HasBetaEquiv.lean
index e35f7ec01..f26424431 100644
--- a/Cslib/Foundations/Syntax/HasBetaEquiv.lean
+++ b/Cslib/Foundations/Syntax/HasBetaEquiv.lean
@@ -13,9 +13,9 @@ public section
 namespace Cslib
 
 /-- Typeclass for the β-equivalence notation `x =β y`. -/
-class HasBetaEquiv (β : Type u) where
-  /-- β-equivalence relation for type β. -/
-  BetaEquiv : β → β → Prop
+class HasBetaEquiv (α : Type u) where
+  /-- β-equivalence relation for type α. -/
+  BetaEquiv : α → α → Prop
 
 @[inherit_doc]
 notation m:max " =β " n:max => HasBetaEquiv.BetaEquiv m n
diff --git a/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean b/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean
index 2c0933a77..310b6f9bd 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean
@@ -35,7 +35,7 @@ namespace LambdaCalculus.Named.Coc
 inductive Term (Var : Type u) : Type u
   | var : Var → Term Var
   | app : Term Var → Term Var → Term Var
-  | lam : Var → Term Var → Term Var → Term Var
+  | abs : Var → Term Var → Term Var → Term Var
   | pi : Var → Term Var → Term Var → Term Var
   | type : Term Var
 deriving DecidableEq
@@ -46,7 +46,7 @@ namespace Term
 def rename [DecidableEq Var] (m : Term Var) (x : Var) (y : Var) : Term Var := match m with
   | .var z => if z = x then .var y else .var z
   | .app f a => .app (f.rename x y) (a.rename x y)
-  | .lam v t b => .lam v (t.rename x y) (b.rename x y)
+  | .abs v t b => .abs v (t.rename x y) (b.rename x y)
   | .pi v t b => .pi v (t.rename x y) (b.rename x y)
   | .type => .type
 
@@ -59,7 +59,7 @@ theorem rename.eq_sizeOf {m : Term Var} {x y : Var} [DecidableEq Var] :
 def fv [DecidableEq Var] : Term Var → Finset Var
   | .var z => {z}
   | .app f a => f.fv ∪ a.fv
-  | .lam v t b => (t.fv ∪ b.fv).erase v
+  | .abs v t b => (t.fv ∪ b.fv).erase v
   | .pi v t b => (t.fv ∪ b.fv).erase v
   | .type => ∅
 
@@ -67,7 +67,7 @@ def fv [DecidableEq Var] : Term Var → Finset Var
 def bv [DecidableEq Var] : Term Var → Finset Var
   | .var _ => ∅
   | .app f a => f.bv ∪ a.bv
-  | .lam v t b => (t.bv ∪ b.bv) ∪ {v}
+  | .abs v t b => (t.bv ∪ b.bv) ∪ {v}
   | .pi v t b => (t.bv ∪ b.bv) ∪ {v}
   | .type => ∅
 
@@ -82,14 +82,14 @@ def subst [DecidableEq Var] [HasFresh Var] (m : Term Var) (x : Var) (r : Term Va
   match m with
   | .var z => if z = x then r else .var z
   | .app f a => .app (f.subst x r) (a.subst x r)
-  | .lam y t b =>
+  | .abs y t b =>
     if y = x then
-      .lam y (t.subst x r) b
+      .abs y (t.subst x r) b
     else if y ∉ r.fv then
-      .lam y (t.subst x r) (b.subst x r)
+      .abs y (t.subst x r) (b.subst x r)
     else
       let z := HasFresh.fresh (t.vars ∪ b.vars ∪ r.vars ∪ {y})
-      .lam z ((t.rename y z).subst x r) ((b.rename y z).subst x r)
+      .abs z ((t.rename y z).subst x r) ((b.rename y z).subst x r)
   | .pi y t b =>
     if y = x then
       .pi y (t.subst x r) b
@@ -110,7 +110,7 @@ instance instHasSubstitutionTerm [DecidableEq Var] [HasFresh Var] :
 /-- β-equivalence. -/
 inductive BetaEquiv [DecidableEq Var] [HasFresh Var] : Term Var → Term Var → Prop
   /-- Equivalance -/
-  | eq : BetaEquiv (B [x := N]) (.app (.lam x A B) N)
+  | eq : BetaEquiv (B [x := N]) (.app (.abs x A B) N)
   /-- Congruence -/
   | cong : BetaEquiv B A → BetaEquiv N M → BetaEquiv (.app B N) (.app A M)
 
@@ -124,7 +124,7 @@ inductive Typing [DecidableEq v] [HasFresh v] : List (v × Term v) → Term v 
   /-- Function application -/
   | app : Typing Γ M (.pi x A B) → Typing Γ N A → Typing Γ (.app M N) (B[x := N])
   /-- Lambda -/
-  | lam : Typing Γ A K → Typing (⟨x, A⟩ :: Γ) N B → Typing Γ (.lam x A N) (.pi x A B)
+  | abs : Typing Γ A K → Typing (⟨x, A⟩ :: Γ) N B → Typing Γ (.abs x A N) (.pi x A B)
   /-- Pi -/
   | pi : Typing Γ A K → Typing (⟨x, A⟩ :: Γ) B L → Typing Γ (.pi x A B) L
   /-- Type -/

From 29c2bd904e55d3e274bf16a56151e4d91dd2240b Mon Sep 17 00:00:00 2001
From: Matt Hunzinger <matt@hunzinger.me>
Date: Tue, 3 Mar 2026 15:18:28 -0500
Subject: [PATCH 07/17] fix: BetaEq relationship order in eq

---
 Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean b/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean
index 310b6f9bd..175636817 100644
--- a/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean
+++ b/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean
@@ -110,7 +110,7 @@ instance instHasSubstitutionTerm [DecidableEq Var] [HasFresh Var] :
 /-- β-equivalence. -/
 inductive BetaEquiv [DecidableEq Var] [HasFresh Var] : Term Var → Term Var → Prop
   /-- Equivalance -/
-  | eq : BetaEquiv (B [x := N]) (.app (.abs x A B) N)
+  | eq : BetaEquiv (.app (.abs x A B) N) (B [x := N])
   /-- Congruence -/
   | cong : BetaEquiv B A → BetaEquiv N M → BetaEquiv (.app B N) (.app A M)
 

From b3c0b23b1e2c45ccb112268c0816be0ec037ade0 Mon Sep 17 00:00:00 2001
From: Matt Hunzinger <matt@hunzinger.me>
Date: Tue, 3 Mar 2026 19:44:30 -0500
Subject: [PATCH 08/17] feat: switch to locally-nameless representation

---
 .../LocallyNameless/Coc/Basic.lean            | 129 ++++++++++++++++
 .../LambdaCalculus/Named/Coc/Basic.lean       | 139 ------------------
 2 files changed, 129 insertions(+), 139 deletions(-)
 create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean
 delete mode 100644 Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean
new file mode 100644
index 000000000..5b21c4ef7
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean
@@ -0,0 +1,129 @@
+/-
+Copyright (c) 2026 Matt Hunzinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Matt Hunzinger
+-/
+
+module
+
+public import Cslib.Foundations.Data.HasFresh
+public import Cslib.Foundations.Syntax.HasAlphaEquiv
+public import Cslib.Foundations.Syntax.HasBetaEquiv
+public import Cslib.Foundations.Syntax.HasSubstitution
+
+@[expose] public section
+
+/-! # Calculus of Constructions
+
+The Calculus of Constructions
+
+## References
+
+* [T. Coquand, *An algorithm for type-checking dependent types*][Coquand1996]
+
+-/
+
+namespace Cslib
+
+universe u
+
+variable {Var : Type u}
+
+namespace LambdaCalculus.LocallyNameless.Coc
+
+/-- Syntax of locally nameless terms, with free variables over `Var`. -/
+inductive Term (Var : Type u) : Type u
+  /-- Bound term variables using a de-Bruijn index. -/
+  | bvar : ℕ → Term Var
+  /-- Free term variables. -/
+  | fvar : Var → Term Var
+  /-- Function application. -/
+  | app : Term Var → Term Var → Term Var
+  /-- Lambda abstraction. -/
+  | abs : Term Var → Term Var → Term Var
+  /-- Pi type. -/
+  | pi : Term Var → Term Var → Term Var
+  /-- Type universe. -/
+  | type : Term Var
+deriving DecidableEq
+
+namespace Term
+
+/-- Free variables. -/
+def fv [DecidableEq Var] : Term Var → Finset Var
+  | .bvar _ => ∅
+  | .fvar z => {z}
+  | .app f a => f.fv ∪ a.fv
+  | .abs t b => t.fv ∪ b.fv
+  | .pi t b => t.fv ∪ b.fv
+  | .type => ∅
+
+/-- Variable opening of the ith bound variable. -/
+def openingRec (i : ℕ) (s : Term Var) : Term Var → Term Var
+  | .bvar y => if i = y then s else (bvar y)
+  | .fvar x => fvar x
+  | .app f a => .app (openingRec i s f) (openingRec i s a)
+  | .abs σ t₁ => abs σ (openingRec (i + 1) s t₁)
+  | .pi σ t₁ => .pi σ (openingRec (i + 1) s t₁)
+  | .type => .type
+
+/-- Variable opening of the closest binding. -/
+def opening (s : Term Var) : Term Var → Term Var := openingRec 0 s
+
+@[inherit_doc]
+scoped infixr:80 " ^ᵗ " => opening
+
+/--
+Capture-avoiding substitution.
+`m.subst x r` replaces the free occurrences of variable `x` in `m` with `r`.
+-/
+def subst [DecidableEq Var] (m : Term Var) (x : Var) (r : Term Var) : Term Var :=
+  match m with
+  | .bvar n => .bvar n
+  | .fvar z => if z = x then r else .fvar z
+  | .app f a => .app (f.subst x r) (a.subst x r)
+  | .abs t b => .abs (t.subst x r) (b.subst x r)
+  | .pi t b => .pi (t.subst x r) (b.subst x r)
+  | .type => .type
+
+/-- `Term.subst` is a substitution for λ-terms. Gives access to the notation `m[x := n]`. -/
+instance instHasSubstitutionTerm [DecidableEq Var] :
+    HasSubstitution (Term Var) Var (Term Var) where
+  subst := Term.subst
+
+/-- β-equivalence. -/
+inductive BetaEquiv : Term Var → Term Var → Prop
+  /-- Equivalance -/
+  | eq : BetaEquiv (.app (.abs A B) N) (B ^ᵗ N)
+  /-- Congruence -/
+  | cong : BetaEquiv B A → BetaEquiv N M → BetaEquiv (.app B N) (.app A M)
+
+instance instHasBetaEquivTerm : HasBetaEquiv (Term Var) where
+  BetaEquiv := BetaEquiv
+
+/-- Typing judgement -/
+inductive Typing [DecidableEq v] : List (v × Term v) → Term v → Term v → Prop
+  /-- Variable lookup in Γ -/
+  | var : ⟨x, A⟩ ∈ Γ → Typing Γ (.fvar x) A
+  /-- Function application -/
+  | app : Typing Γ M (.pi A B) → Typing Γ N A → Typing Γ (.app M N) (B ^ᵗ N)
+  /-- Lambda abstraction -/
+  | abs (ρ : Finset v) :
+      Typing Γ A K →
+      (∀ x ∉ ρ, Typing (⟨x, A⟩ :: Γ) (N ^ᵗ .fvar x) (B ^ᵗ .fvar x)) →
+      Typing Γ (.abs A N) (.pi A B)
+  /-- Pi type -/
+  | pi (ρ : Finset v) :
+      Typing Γ A K →
+      (∀ x ∉ ρ, Typing (⟨x, A⟩ :: Γ) (B ^ᵗ .fvar x) L) →
+      Typing Γ (.pi A B) L
+  /-- Type universe -/
+  | type : Typing Γ .type .type
+  /-- β-conversion -/
+  | conv : Typing Γ M A → A =β B → Typing Γ M B
+
+end Term
+
+end LambdaCalculus.LocallyNameless.Coc
+
+end Cslib
diff --git a/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean b/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean
deleted file mode 100644
index 175636817..000000000
--- a/Cslib/Languages/LambdaCalculus/Named/Coc/Basic.lean
+++ /dev/null
@@ -1,139 +0,0 @@
-/-
-Copyright (c) 2026 Matt Hunzinger. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Matt Hunzinger
--/
-
-module
-
-public import Cslib.Foundations.Data.HasFresh
-public import Cslib.Foundations.Syntax.HasAlphaEquiv
-public import Cslib.Foundations.Syntax.HasBetaEquiv
-public import Cslib.Foundations.Syntax.HasSubstitution
-
-@[expose] public section
-
-/-! # Calculus of Constructions
-
-The Calculus of Constructions
-
-## References
-
-* [T. Coquand, *An algorithm for type-checking dependent types*][Coquand1996]
-
--/
-
-namespace Cslib
-
-universe u
-
-variable {Var : Type u}
-
-namespace LambdaCalculus.Named.Coc
-
-/-- Syntax of terms. -/
-inductive Term (Var : Type u) : Type u
-  | var : Var → Term Var
-  | app : Term Var → Term Var → Term Var
-  | abs : Var → Term Var → Term Var → Term Var
-  | pi : Var → Term Var → Term Var → Term Var
-  | type : Term Var
-deriving DecidableEq
-
-namespace Term
-
-/-- Renaming, or variable substitution. `m.rename x y` renames `x` into `y` in `m`. -/
-def rename [DecidableEq Var] (m : Term Var) (x : Var) (y : Var) : Term Var := match m with
-  | .var z => if z = x then .var y else .var z
-  | .app f a => .app (f.rename x y) (a.rename x y)
-  | .abs v t b => .abs v (t.rename x y) (b.rename x y)
-  | .pi v t b => .pi v (t.rename x y) (b.rename x y)
-  | .type => .type
-
-/-- Renaming preserves size. -/
-theorem rename.eq_sizeOf {m : Term Var} {x y : Var} [DecidableEq Var] :
-    sizeOf (m.rename x y) = sizeOf m := by
-  induction m <;> simp_all [Term.rename] ; split <;> simp_all
-
-/-- Free variables. -/
-def fv [DecidableEq Var] : Term Var → Finset Var
-  | .var z => {z}
-  | .app f a => f.fv ∪ a.fv
-  | .abs v t b => (t.fv ∪ b.fv).erase v
-  | .pi v t b => (t.fv ∪ b.fv).erase v
-  | .type => ∅
-
-/-- Bound variables. -/
-def bv [DecidableEq Var] : Term Var → Finset Var
-  | .var _ => ∅
-  | .app f a => f.bv ∪ a.bv
-  | .abs v t b => (t.bv ∪ b.bv) ∪ {v}
-  | .pi v t b => (t.bv ∪ b.bv) ∪ {v}
-  | .type => ∅
-
-/-- Variable names (free and bound) in a term. -/
-def vars [DecidableEq Var] (t : Term Var) : Finset Var := t.fv ∪ t.bv
-
-/--
-Capture-avoiding substitution.
-`m.subst x r` replaces the free occurrences of variable `x` in `m` with `r`.
--/
-def subst [DecidableEq Var] [HasFresh Var] (m : Term Var) (x : Var) (r : Term Var) : Term Var :=
-  match m with
-  | .var z => if z = x then r else .var z
-  | .app f a => .app (f.subst x r) (a.subst x r)
-  | .abs y t b =>
-    if y = x then
-      .abs y (t.subst x r) b
-    else if y ∉ r.fv then
-      .abs y (t.subst x r) (b.subst x r)
-    else
-      let z := HasFresh.fresh (t.vars ∪ b.vars ∪ r.vars ∪ {y})
-      .abs z ((t.rename y z).subst x r) ((b.rename y z).subst x r)
-  | .pi y t b =>
-    if y = x then
-      .pi y (t.subst x r) b
-    else if y ∉ r.fv then
-      .pi y (t.subst x r) (b.subst x r)
-    else
-      let z := HasFresh.fresh (t.vars ∪ b.vars ∪ r.vars ∪ {y})
-      .pi z ((t.rename y z).subst x r) ((b.rename y z).subst x r)
-  | .type => .type
-  termination_by m
-  decreasing_by all_goals grind [rename.eq_sizeOf]
-
-/-- `Term.subst` is a substitution for λ-terms. Gives access to the notation `m[x := n]`. -/
-instance instHasSubstitutionTerm [DecidableEq Var] [HasFresh Var] :
-    HasSubstitution (Term Var) Var (Term Var) where
-  subst := Term.subst
-
-/-- β-equivalence. -/
-inductive BetaEquiv [DecidableEq Var] [HasFresh Var] : Term Var → Term Var → Prop
-  /-- Equivalance -/
-  | eq : BetaEquiv (.app (.abs x A B) N) (B [x := N])
-  /-- Congruence -/
-  | cong : BetaEquiv B A → BetaEquiv N M → BetaEquiv (.app B N) (.app A M)
-
-instance instHasBetaEquivTerm [DecidableEq Var] [HasFresh Var] : HasBetaEquiv (Term Var) where
-  BetaEquiv := BetaEquiv
-
-/-- Typing judgement -/
-inductive Typing [DecidableEq v] [HasFresh v] : List (v × Term v) → Term v → Term v → Prop
-  /-- Variable lookup in Γ -/
-  | var : ⟨x, A⟩ ∈ Γ → Typing Γ (.var x) A
-  /-- Function application -/
-  | app : Typing Γ M (.pi x A B) → Typing Γ N A → Typing Γ (.app M N) (B[x := N])
-  /-- Lambda -/
-  | abs : Typing Γ A K → Typing (⟨x, A⟩ :: Γ) N B → Typing Γ (.abs x A N) (.pi x A B)
-  /-- Pi -/
-  | pi : Typing Γ A K → Typing (⟨x, A⟩ :: Γ) B L → Typing Γ (.pi x A B) L
-  /-- Type -/
-  | type : Typing Γ .type .type
-  /-- Conversion -/
-  | conv : Typing Γ M A → A =β B → Typing Γ M B
-
-end Term
-
-end LambdaCalculus.Named.Coc
-
-end Cslib

From 8a207525913f794a926305b879df60f5251bc631 Mon Sep 17 00:00:00 2001
From: Matt Hunzinger <matt@hunzinger.me>
Date: Tue, 3 Mar 2026 23:26:53 -0500
Subject: [PATCH 09/17] feat: add opening lemmas for locally-closed terms and
 split up code into new files

---
 .../LocallyNameless/Coc/Basic.lean            |  76 +----------
 .../LocallyNameless/Coc/Opening.lean          | 121 ++++++++++++++++++
 .../LocallyNameless/Coc/Typing.lean           |  68 ++++++++++
 3 files changed, 191 insertions(+), 74 deletions(-)
 create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean
 create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Typing.lean

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean
index 5b21c4ef7..ff00ed17a 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean
@@ -7,9 +7,6 @@ Authors: Matt Hunzinger
 module
 
 public import Cslib.Foundations.Data.HasFresh
-public import Cslib.Foundations.Syntax.HasAlphaEquiv
-public import Cslib.Foundations.Syntax.HasBetaEquiv
-public import Cslib.Foundations.Syntax.HasSubstitution
 
 @[expose] public section
 
@@ -27,8 +24,6 @@ namespace Cslib
 
 universe u
 
-variable {Var : Type u}
-
 namespace LambdaCalculus.LocallyNameless.Coc
 
 /-- Syntax of locally nameless terms, with free variables over `Var`. -/
@@ -47,10 +42,9 @@ inductive Term (Var : Type u) : Type u
   | type : Term Var
 deriving DecidableEq
 
-namespace Term
-
 /-- Free variables. -/
-def fv [DecidableEq Var] : Term Var → Finset Var
+@[scoped grind =]
+def Term.fv [DecidableEq Var] : Term Var → Finset Var
   | .bvar _ => ∅
   | .fvar z => {z}
   | .app f a => f.fv ∪ a.fv
@@ -58,72 +52,6 @@ def fv [DecidableEq Var] : Term Var → Finset Var
   | .pi t b => t.fv ∪ b.fv
   | .type => ∅
 
-/-- Variable opening of the ith bound variable. -/
-def openingRec (i : ℕ) (s : Term Var) : Term Var → Term Var
-  | .bvar y => if i = y then s else (bvar y)
-  | .fvar x => fvar x
-  | .app f a => .app (openingRec i s f) (openingRec i s a)
-  | .abs σ t₁ => abs σ (openingRec (i + 1) s t₁)
-  | .pi σ t₁ => .pi σ (openingRec (i + 1) s t₁)
-  | .type => .type
-
-/-- Variable opening of the closest binding. -/
-def opening (s : Term Var) : Term Var → Term Var := openingRec 0 s
-
-@[inherit_doc]
-scoped infixr:80 " ^ᵗ " => opening
-
-/--
-Capture-avoiding substitution.
-`m.subst x r` replaces the free occurrences of variable `x` in `m` with `r`.
--/
-def subst [DecidableEq Var] (m : Term Var) (x : Var) (r : Term Var) : Term Var :=
-  match m with
-  | .bvar n => .bvar n
-  | .fvar z => if z = x then r else .fvar z
-  | .app f a => .app (f.subst x r) (a.subst x r)
-  | .abs t b => .abs (t.subst x r) (b.subst x r)
-  | .pi t b => .pi (t.subst x r) (b.subst x r)
-  | .type => .type
-
-/-- `Term.subst` is a substitution for λ-terms. Gives access to the notation `m[x := n]`. -/
-instance instHasSubstitutionTerm [DecidableEq Var] :
-    HasSubstitution (Term Var) Var (Term Var) where
-  subst := Term.subst
-
-/-- β-equivalence. -/
-inductive BetaEquiv : Term Var → Term Var → Prop
-  /-- Equivalance -/
-  | eq : BetaEquiv (.app (.abs A B) N) (B ^ᵗ N)
-  /-- Congruence -/
-  | cong : BetaEquiv B A → BetaEquiv N M → BetaEquiv (.app B N) (.app A M)
-
-instance instHasBetaEquivTerm : HasBetaEquiv (Term Var) where
-  BetaEquiv := BetaEquiv
-
-/-- Typing judgement -/
-inductive Typing [DecidableEq v] : List (v × Term v) → Term v → Term v → Prop
-  /-- Variable lookup in Γ -/
-  | var : ⟨x, A⟩ ∈ Γ → Typing Γ (.fvar x) A
-  /-- Function application -/
-  | app : Typing Γ M (.pi A B) → Typing Γ N A → Typing Γ (.app M N) (B ^ᵗ N)
-  /-- Lambda abstraction -/
-  | abs (ρ : Finset v) :
-      Typing Γ A K →
-      (∀ x ∉ ρ, Typing (⟨x, A⟩ :: Γ) (N ^ᵗ .fvar x) (B ^ᵗ .fvar x)) →
-      Typing Γ (.abs A N) (.pi A B)
-  /-- Pi type -/
-  | pi (ρ : Finset v) :
-      Typing Γ A K →
-      (∀ x ∉ ρ, Typing (⟨x, A⟩ :: Γ) (B ^ᵗ .fvar x) L) →
-      Typing Γ (.pi A B) L
-  /-- Type universe -/
-  | type : Typing Γ .type .type
-  /-- β-conversion -/
-  | conv : Typing Γ M A → A =β B → Typing Γ M B
-
-end Term
-
 end LambdaCalculus.LocallyNameless.Coc
 
 end Cslib
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean
new file mode 100644
index 000000000..fb5793510
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean
@@ -0,0 +1,121 @@
+/-
+Copyright (c) 2026 Matt Hunzinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Matt Hunzinger
+-/
+
+module
+
+public import Cslib.Foundations.Data.HasFresh
+public import Cslib.Foundations.Syntax.HasSubstitution
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Coc.Basic
+
+@[expose] public section
+
+/-! # Calculus of Constructions
+
+The Calculus of Constructions
+
+## References
+
+* [T. Coquand, *An algorithm for type-checking dependent types*][Coquand1996]
+
+-/
+
+namespace Cslib
+
+universe u
+
+namespace LambdaCalculus.LocallyNameless.Coc
+
+namespace Term
+
+/-- Variable opening of the ith bound variable. -/
+@[scoped grind =]
+def openingRec (i : ℕ) (s : Term Var) : Term Var → Term Var
+  | .bvar y => if i = y then s else (bvar y)
+  | .fvar x => fvar x
+  | .app f a => .app (openingRec i s f) (openingRec i s a)
+  | .abs σ t₁ => abs (openingRec i s σ) (openingRec (i + 1) s t₁)
+  | .pi σ t₁ => .pi (openingRec i s σ) (openingRec (i + 1) s t₁)
+  | .type => .type
+
+/-- Variable opening of the closest binding. -/
+@[scoped grind =]
+def opening (s : Term Var) (t : Term Var) : Term Var := openingRec 0 t s
+
+@[inherit_doc]
+scoped infixr:80 " ^ᵗ " => opening
+
+@[inherit_doc]
+scoped notation:68 γ "⟦" X " ↝ " δ "⟧"=> openingRec X δ γ
+
+/--
+Capture-avoiding substitution.
+`m.subst x r` replaces the free occurrences of variable `x` in `m` with `r`.
+-/
+@[scoped grind =]
+def subst [DecidableEq Var] (m : Term Var) (x : Var) (r : Term Var) : Term Var :=
+  match m with
+  | .bvar n => .bvar n
+  | .fvar z => if z = x then r else .fvar z
+  | .app f a => .app (f.subst x r) (a.subst x r)
+  | .abs t b => .abs (t.subst x r) (b.subst x r)
+  | .pi t b => .pi (t.subst x r) (b.subst x r)
+  | .type => .type
+
+/-- `Term.subst` is a substitution for λ-terms. Gives access to the notation `m[x := n]`. -/
+instance instHasSubstitutionTerm [DecidableEq Var] :
+    HasSubstitution (Term Var) Var (Term Var) where
+  subst := Term.subst
+
+@[scoped grind _=_]
+lemma subst_def [DecidableEq Var] :
+    Term.subst (m : Term Var) (x : Var) (r : Term Var) = m[x := r] := rfl
+
+/-- Substitution of a free variable not present in a term leaves it unchanged. -/
+lemma subst_fresh [DecidableEq Var] {γ : Term Var}
+    (nmem : X ∉ γ.fv) (δ : Term Var) : γ = γ[X := δ] := by
+  induction γ <;> grind
+
+/-- An opening appearing in both sides of an equality of terms can be removed. -/
+lemma openingRec_neq_eq (neq : x ≠ y) (eq : t⟦y ↝ s₁⟧ = t⟦y ↝ s₁⟧⟦x ↝ s₂⟧) :
+    t = t⟦x ↝ s₂⟧ := by
+  induction t generalizing x y <;> grind
+
+/-- Locally closed terms. -/
+inductive LC : Term Var → Prop
+  | var : LC (.fvar x)
+  | app : LC t₁ → LC t₂ → LC (app t₁ t₂)
+  | abs (L : Finset Var) : σ.LC → (∀ x ∉ L, LC (t₁ ^ᵗ fvar x)) → LC (abs σ t₁)
+  | pi (L : Finset Var) : σ.LC → (∀ x ∉ L, LC (t₁ ^ᵗ fvar x)) → LC (pi σ t₁)
+  | type : LC .type
+
+attribute [scoped grind .] LC.var LC.app LC.type
+
+/-- A locally closed term is unchanged by opening. -/
+lemma openingRec_lc [HasFresh Var] {σ τ : Term Var} (lc : σ.LC) : σ = σ⟦X ↝ τ⟧ := by
+  classical
+  induction lc generalizing X with
+  | abs | pi => grind [fresh_exists <| free_union Var, openingRec_neq_eq]
+  | _ => grind
+
+/-- Substitution of a locally closed type distributes with opening. -/
+lemma openingRec_subst [DecidableEq Var] [HasFresh Var] {δ : Term Var}
+    (Y : ℕ) (σ τ : Term Var) (lc : δ.LC) (X : Var) :
+    (σ⟦Y ↝ τ⟧)[X := δ] = σ[X := δ]⟦Y ↝ τ[X := δ]⟧ := by
+  induction σ generalizing Y <;> grind [openingRec_lc]
+
+/-- A locally closed term remains locally closed after substitution. -/
+lemma subst_lc [DecidableEq Var] [HasFresh Var] {σ τ : Term Var}
+    (σ_lc : σ.LC) (τ_lc : τ.LC) (X : Var) : σ[X := τ].LC := by
+  induction σ_lc with
+  | abs => grind [LC.abs (free_union Var), openingRec_subst]
+  | pi => grind [LC.pi (free_union Var), openingRec_subst]
+  | _ => grind [openingRec_subst]
+
+end Term
+
+end LambdaCalculus.LocallyNameless.Coc
+
+end Cslib
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Typing.lean
new file mode 100644
index 000000000..dd947b568
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Typing.lean
@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2026 Matt Hunzinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Matt Hunzinger
+-/
+
+module
+
+public import Cslib.Foundations.Data.HasFresh
+public import Cslib.Foundations.Syntax.HasAlphaEquiv
+public import Cslib.Foundations.Syntax.HasBetaEquiv
+public import Cslib.Foundations.Syntax.HasSubstitution
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Coc.Opening
+
+@[expose] public section
+
+/-! # Calculus of Constructions
+
+The Calculus of Constructions
+
+## References
+
+* [T. Coquand, *An algorithm for type-checking dependent types*][Coquand1996]
+
+-/
+
+namespace Cslib
+
+universe u
+
+namespace LambdaCalculus.LocallyNameless.Coc
+
+open Term
+
+/-- β-equivalence. -/
+inductive BetaEquiv : Term Var → Term Var → Prop
+  /-- Equivalance -/
+  | eq : BetaEquiv (.app (.abs A B) N) (B ^ᵗ N)
+  /-- Congruence -/
+  | cong : BetaEquiv B A → BetaEquiv N M → BetaEquiv (.app B N) (.app A M)
+
+instance instHasBetaEquivTerm : HasBetaEquiv (Term Var) where
+  BetaEquiv := BetaEquiv
+
+/-- Typing judgement -/
+inductive Typing [DecidableEq v] : List (v × Term v) → Term v → Term v → Prop
+  /-- Variable lookup in Γ -/
+  | var : ⟨x, A⟩ ∈ Γ → Typing Γ (.fvar x) A
+  /-- Function application -/
+  | app : Typing Γ M (.pi A B) → Typing Γ N A → Typing Γ (.app M N) (B ^ᵗ N)
+  /-- Lambda abstraction -/
+  | abs (ρ : Finset v) :
+      Typing Γ A K →
+      (∀ x ∉ ρ, Typing (⟨x, A⟩ :: Γ) (N ^ᵗ .fvar x) (B ^ᵗ .fvar x)) →
+      Typing Γ (.abs A N) (.pi A B)
+  /-- Pi type -/
+  | pi (ρ : Finset v) :
+      Typing Γ A K →
+      (∀ x ∉ ρ, Typing (⟨x, A⟩ :: Γ) (B ^ᵗ .fvar x) L) →
+      Typing Γ (.pi A B) L
+  /-- Type universe -/
+  | type : Typing Γ .type .type
+  /-- β-conversion -/
+  | conv : Typing Γ M A → A =β B → Typing Γ M B
+
+end LambdaCalculus.LocallyNameless.Coc
+
+end Cslib

From 13ec089f2f49234b5402b07a9c1d306e8f70d6b0 Mon Sep 17 00:00:00 2001
From: Matt Hunzinger <matt@hunzinger.me>
Date: Tue, 3 Mar 2026 23:52:49 -0500
Subject: [PATCH 10/17] feat: WellFormed

---
 .../LocallyNameless/Coc/Basic.lean            |  4 ++
 .../LocallyNameless/Coc/Typing.lean           | 14 ++---
 .../LocallyNameless/Coc/WellFormed.lean       | 58 +++++++++++++++++++
 3 files changed, 69 insertions(+), 7 deletions(-)
 create mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/WellFormed.lean

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean
index ff00ed17a..c24a69f00 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean
@@ -52,6 +52,10 @@ def Term.fv [DecidableEq Var] : Term Var → Finset Var
   | .pi t b => t.fv ∪ b.fv
   | .type => ∅
 
+abbrev Env (Var : Type u) := Finset (Var × Term Var)
+
+def Env.dom [DecidableEq Var] : Env Var → Finset Var := Finset.image Prod.fst
+
 end LambdaCalculus.LocallyNameless.Coc
 
 end Cslib
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Typing.lean
index dd947b568..d90645505 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Typing.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Typing.lean
@@ -10,7 +10,7 @@ public import Cslib.Foundations.Data.HasFresh
 public import Cslib.Foundations.Syntax.HasAlphaEquiv
 public import Cslib.Foundations.Syntax.HasBetaEquiv
 public import Cslib.Foundations.Syntax.HasSubstitution
-public import Cslib.Languages.LambdaCalculus.LocallyNameless.Coc.Opening
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Coc.WellFormed
 
 @[expose] public section
 
@@ -43,20 +43,20 @@ instance instHasBetaEquivTerm : HasBetaEquiv (Term Var) where
   BetaEquiv := BetaEquiv
 
 /-- Typing judgement -/
-inductive Typing [DecidableEq v] : List (v × Term v) → Term v → Term v → Prop
+inductive Typing [DecidableEq Var] : Env Var → Term Var → Term Var → Prop
   /-- Variable lookup in Γ -/
-  | var : ⟨x, A⟩ ∈ Γ → Typing Γ (.fvar x) A
+  | var : Γ.Wf → ⟨x, A⟩ ∈ Γ → Typing Γ (.fvar x) A
   /-- Function application -/
   | app : Typing Γ M (.pi A B) → Typing Γ N A → Typing Γ (.app M N) (B ^ᵗ N)
   /-- Lambda abstraction -/
-  | abs (ρ : Finset v) :
+  | abs (ρ : Finset Var) :
       Typing Γ A K →
-      (∀ x ∉ ρ, Typing (⟨x, A⟩ :: Γ) (N ^ᵗ .fvar x) (B ^ᵗ .fvar x)) →
+      (∀ x ∉ ρ, Typing ({⟨x, A⟩} ∪ Γ) (N ^ᵗ .fvar x) (B ^ᵗ .fvar x)) →
       Typing Γ (.abs A N) (.pi A B)
   /-- Pi type -/
-  | pi (ρ : Finset v) :
+  | pi (ρ : Finset Var) :
       Typing Γ A K →
-      (∀ x ∉ ρ, Typing (⟨x, A⟩ :: Γ) (B ^ᵗ .fvar x) L) →
+      (∀ x ∉ ρ, Typing ({⟨x, A⟩} ∪ Γ) (B ^ᵗ .fvar x) L) →
       Typing Γ (.pi A B) L
   /-- Type universe -/
   | type : Typing Γ .type .type
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/WellFormed.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/WellFormed.lean
new file mode 100644
index 000000000..31d4a8f84
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/WellFormed.lean
@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2026 Matt Hunzinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Matt Hunzinger
+-/
+
+module
+
+public import Cslib.Foundations.Data.HasFresh
+public import Cslib.Foundations.Syntax.HasSubstitution
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Coc.Opening
+
+@[expose] public section
+
+/-! # Calculus of Constructions
+
+The Calculus of Constructions
+
+## References
+
+* [T. Coquand, *An algorithm for type-checking dependent types*][Coquand1996]
+
+-/
+
+namespace Cslib
+
+universe u
+
+variable {Var : Type u} [DecidableEq Var]
+
+namespace LambdaCalculus.LocallyNameless.Coc
+
+namespace Term
+
+/-- Well-formedness of terms. -/
+inductive Wf : Env Var → Term Var → Prop
+  | var : ⟨x, _⟩ ∈ Γ → Wf Γ (.fvar x)
+  | app : Wf Γ f → Wf Γ a → Wf Γ (.app f a)
+  | abs (L : Finset Var) :
+      Wf Γ σ →
+      (∀ X ∉ L, Wf ({⟨X,σ⟩} ∪ Γ) (τ ^ᵗ fvar X)) →
+      Wf Γ (abs σ τ)
+  | pi (L : Finset Var) :
+      Wf Γ σ →
+      (∀ X ∉ L, Wf ({⟨X,σ⟩} ∪ Γ) (τ ^ᵗ fvar X)) →
+      Wf Γ (pi σ τ)
+  | type : Wf Γ .type
+
+end Term
+
+/-- An environment is well-formed if it binds each variable exactly once to a well-formed type. -/
+inductive Env.Wf : Env Var → Prop
+  | nil : Wf {}
+  | cons : Wf Γ → Term.Wf Γ τ → x ∉ Γ.dom → Wf ({⟨x, τ⟩} ∪ Γ)
+
+end LambdaCalculus.LocallyNameless.Coc
+
+end Cslib

From 0d6e3b9d7de50b478f3f06643ec9bedfd27d97a6 Mon Sep 17 00:00:00 2001
From: Matt Hunzinger <matt@hunzinger.me>
Date: Wed, 4 Mar 2026 12:24:15 -0500
Subject: [PATCH 11/17] refactor: re-use existing Context for Env

---
 .../Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean  | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean
index c24a69f00..e8668dbc4 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean
@@ -7,6 +7,7 @@ Authors: Matt Hunzinger
 module
 
 public import Cslib.Foundations.Data.HasFresh
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Context
 
 @[expose] public section
 
@@ -52,9 +53,7 @@ def Term.fv [DecidableEq Var] : Term Var → Finset Var
   | .pi t b => t.fv ∪ b.fv
   | .type => ∅
 
-abbrev Env (Var : Type u) := Finset (Var × Term Var)
-
-def Env.dom [DecidableEq Var] : Env Var → Finset Var := Finset.image Prod.fst
+abbrev Env (Var : Type u) := Context Var (Term Var)
 
 end LambdaCalculus.LocallyNameless.Coc
 

From 52d3606af29879bdad088551da08c57c7b4d17b7 Mon Sep 17 00:00:00 2001
From: Matt Hunzinger <matt@hunzinger.me>
Date: Wed, 4 Mar 2026 12:26:47 -0500
Subject: [PATCH 12/17] refactor: rename opening to open' to match current
 conventions

---
 .../LocallyNameless/Coc/Opening.lean          | 30 +++++++++----------
 1 file changed, 15 insertions(+), 15 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean
index fb5793510..d9de2b1a7 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean
@@ -32,23 +32,23 @@ namespace Term
 
 /-- Variable opening of the ith bound variable. -/
 @[scoped grind =]
-def openingRec (i : ℕ) (s : Term Var) : Term Var → Term Var
+def openRec (i : ℕ) (s : Term Var) : Term Var → Term Var
   | .bvar y => if i = y then s else (bvar y)
   | .fvar x => fvar x
-  | .app f a => .app (openingRec i s f) (openingRec i s a)
-  | .abs σ t₁ => abs (openingRec i s σ) (openingRec (i + 1) s t₁)
-  | .pi σ t₁ => .pi (openingRec i s σ) (openingRec (i + 1) s t₁)
+  | .app f a => .app (openRec i s f) (openRec i s a)
+  | .abs σ t₁ => abs (openRec i s σ) (openRec (i + 1) s t₁)
+  | .pi σ t₁ => .pi (openRec i s σ) (openRec (i + 1) s t₁)
   | .type => .type
 
 /-- Variable opening of the closest binding. -/
 @[scoped grind =]
-def opening (s : Term Var) (t : Term Var) : Term Var := openingRec 0 t s
+def open' (s : Term Var) (t : Term Var) : Term Var := openRec 0 t s
 
 @[inherit_doc]
-scoped infixr:80 " ^ᵗ " => opening
+scoped infixr:80 " ^ᵗ " => open'
 
 @[inherit_doc]
-scoped notation:68 γ "⟦" X " ↝ " δ "⟧"=> openingRec X δ γ
+scoped notation:68 γ "⟦" X " ↝ " δ "⟧"=> openRec X δ γ
 
 /--
 Capture-avoiding substitution.
@@ -79,7 +79,7 @@ lemma subst_fresh [DecidableEq Var] {γ : Term Var}
   induction γ <;> grind
 
 /-- An opening appearing in both sides of an equality of terms can be removed. -/
-lemma openingRec_neq_eq (neq : x ≠ y) (eq : t⟦y ↝ s₁⟧ = t⟦y ↝ s₁⟧⟦x ↝ s₂⟧) :
+lemma openRec_neq_eq (neq : x ≠ y) (eq : t⟦y ↝ s₁⟧ = t⟦y ↝ s₁⟧⟦x ↝ s₂⟧) :
     t = t⟦x ↝ s₂⟧ := by
   induction t generalizing x y <;> grind
 
@@ -94,25 +94,25 @@ inductive LC : Term Var → Prop
 attribute [scoped grind .] LC.var LC.app LC.type
 
 /-- A locally closed term is unchanged by opening. -/
-lemma openingRec_lc [HasFresh Var] {σ τ : Term Var} (lc : σ.LC) : σ = σ⟦X ↝ τ⟧ := by
+lemma openRec_lc [HasFresh Var] {σ τ : Term Var} (lc : σ.LC) : σ = σ⟦X ↝ τ⟧ := by
   classical
   induction lc generalizing X with
-  | abs | pi => grind [fresh_exists <| free_union Var, openingRec_neq_eq]
+  | abs | pi => grind [fresh_exists <| free_union Var, openRec_neq_eq]
   | _ => grind
 
 /-- Substitution of a locally closed type distributes with opening. -/
-lemma openingRec_subst [DecidableEq Var] [HasFresh Var] {δ : Term Var}
+lemma openRec_subst [DecidableEq Var] [HasFresh Var] {δ : Term Var}
     (Y : ℕ) (σ τ : Term Var) (lc : δ.LC) (X : Var) :
     (σ⟦Y ↝ τ⟧)[X := δ] = σ[X := δ]⟦Y ↝ τ[X := δ]⟧ := by
-  induction σ generalizing Y <;> grind [openingRec_lc]
+  induction σ generalizing Y <;> grind [openRec_lc]
 
 /-- A locally closed term remains locally closed after substitution. -/
 lemma subst_lc [DecidableEq Var] [HasFresh Var] {σ τ : Term Var}
     (σ_lc : σ.LC) (τ_lc : τ.LC) (X : Var) : σ[X := τ].LC := by
   induction σ_lc with
-  | abs => grind [LC.abs (free_union Var), openingRec_subst]
-  | pi => grind [LC.pi (free_union Var), openingRec_subst]
-  | _ => grind [openingRec_subst]
+  | abs => grind [LC.abs (free_union Var), openRec_subst]
+  | pi => grind [LC.pi (free_union Var), openRec_subst]
+  | _ => grind [openRec_subst]
 
 end Term
 

From 58caddf5abda0c70956f30b6c94b8d87dc068427 Mon Sep 17 00:00:00 2001
From: Matt Hunzinger <matt@hunzinger.me>
Date: Wed, 4 Mar 2026 12:31:37 -0500
Subject: [PATCH 13/17] refactor: rename LC-related variables for clarity

---
 .../LocallyNameless/Coc/Opening.lean             | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean
index d9de2b1a7..f9d7e3215 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean
@@ -87,8 +87,8 @@ lemma openRec_neq_eq (neq : x ≠ y) (eq : t⟦y ↝ s₁⟧ = t⟦y ↝ s₁⟧
 inductive LC : Term Var → Prop
   | var : LC (.fvar x)
   | app : LC t₁ → LC t₂ → LC (app t₁ t₂)
-  | abs (L : Finset Var) : σ.LC → (∀ x ∉ L, LC (t₁ ^ᵗ fvar x)) → LC (abs σ t₁)
-  | pi (L : Finset Var) : σ.LC → (∀ x ∉ L, LC (t₁ ^ᵗ fvar x)) → LC (pi σ t₁)
+  | abs (L : Finset Var) : t₁.LC → (∀ x ∉ L, LC (t₂ ^ᵗ fvar x)) → LC (abs t₁ t₂)
+  | pi (L : Finset Var) : t₁.LC → (∀ x ∉ L, LC (t₂ ^ᵗ fvar x)) → LC (pi t₁ t₂)
   | type : LC .type
 
 attribute [scoped grind .] LC.var LC.app LC.type
@@ -102,14 +102,14 @@ lemma openRec_lc [HasFresh Var] {σ τ : Term Var} (lc : σ.LC) : σ = σ⟦X 
 
 /-- Substitution of a locally closed type distributes with opening. -/
 lemma openRec_subst [DecidableEq Var] [HasFresh Var] {δ : Term Var}
-    (Y : ℕ) (σ τ : Term Var) (lc : δ.LC) (X : Var) :
-    (σ⟦Y ↝ τ⟧)[X := δ] = σ[X := δ]⟦Y ↝ τ[X := δ]⟧ := by
-  induction σ generalizing Y <;> grind [openRec_lc]
+    (Y : ℕ) (t₁ t₂ : Term Var) (lc : δ.LC) (X : Var) :
+    (t₁⟦Y ↝ t₂⟧)[X := δ] = t₁[X := δ]⟦Y ↝ t₂[X := δ]⟧ := by
+  induction t₁ generalizing Y <;> grind [openRec_lc]
 
 /-- A locally closed term remains locally closed after substitution. -/
-lemma subst_lc [DecidableEq Var] [HasFresh Var] {σ τ : Term Var}
-    (σ_lc : σ.LC) (τ_lc : τ.LC) (X : Var) : σ[X := τ].LC := by
-  induction σ_lc with
+lemma subst_lc [DecidableEq Var] [HasFresh Var] {t₁ t₂ : Term Var}
+    (t₁_lc : t₁.LC) (t₂_lc : t₂.LC) (X : Var) : t₁[X := t₂].LC := by
+  induction t₁_lc with
   | abs => grind [LC.abs (free_union Var), openRec_subst]
   | pi => grind [LC.pi (free_union Var), openRec_subst]
   | _ => grind [openRec_subst]

From 827087b5b80da4e39a0ea49551746d328ffdcee5 Mon Sep 17 00:00:00 2001
From: Matt Hunzinger <matt@hunzinger.me>
Date: Wed, 4 Mar 2026 12:33:40 -0500
Subject: [PATCH 14/17] refactor: replace use of classical with constraint on
 DecidableEq to fit current conventions

---
 .../LambdaCalculus/LocallyNameless/Coc/Opening.lean          | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean
index f9d7e3215..ba3054e0b 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean
@@ -22,6 +22,8 @@ The Calculus of Constructions
 
 -/
 
+set_option linter.unusedDecidableInType false
+
 namespace Cslib
 
 universe u
@@ -94,8 +96,7 @@ inductive LC : Term Var → Prop
 attribute [scoped grind .] LC.var LC.app LC.type
 
 /-- A locally closed term is unchanged by opening. -/
-lemma openRec_lc [HasFresh Var] {σ τ : Term Var} (lc : σ.LC) : σ = σ⟦X ↝ τ⟧ := by
-  classical
+lemma openRec_lc [DecidableEq Var] [HasFresh Var] {σ τ : Term Var} (lc : σ.LC) : σ = σ⟦X ↝ τ⟧ := by
   induction lc generalizing X with
   | abs | pi => grind [fresh_exists <| free_union Var, openRec_neq_eq]
   | _ => grind

From d6afe922c4debee2118e62b2c74f09fc72adeb4c Mon Sep 17 00:00:00 2001
From: Matt Hunzinger <matt@hunzinger.me>
Date: Wed, 4 Mar 2026 12:52:42 -0500
Subject: [PATCH 15/17] fix: extend BetaEquiv to match the definition by
 Chargueraud

---
 .../LocallyNameless/Coc/Basic.lean            |  2 ++
 .../LocallyNameless/Coc/Opening.lean          |  6 ++++
 .../LocallyNameless/Coc/Typing.lean           | 28 +++++++++++++++----
 3 files changed, 31 insertions(+), 5 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean
index e8668dbc4..678b1ed48 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean
@@ -19,6 +19,8 @@ The Calculus of Constructions
 
 * [T. Coquand, *An algorithm for type-checking dependent types*][Coquand1996]
 
+* [A. Chargueraud, *The Locally Nameless Representation*][Chargueraud2012]
+
 -/
 
 namespace Cslib
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean
index ba3054e0b..f6bf29eb6 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean
@@ -20,6 +20,8 @@ The Calculus of Constructions
 
 * [T. Coquand, *An algorithm for type-checking dependent types*][Coquand1996]
 
+* [A. Chargueraud, *The Locally Nameless Representation*][Chargueraud2012]
+
 -/
 
 set_option linter.unusedDecidableInType false
@@ -95,6 +97,10 @@ inductive LC : Term Var → Prop
 
 attribute [scoped grind .] LC.var LC.app LC.type
 
+/-- Predicate for being a locally closed body of an abstraction. -/
+@[scoped grind =]
+def body (t : Term Var) := ∃ L : Finset Var, ∀ x ∉ L, LC (t ^ᵗ fvar x)
+
 /-- A locally closed term is unchanged by opening. -/
 lemma openRec_lc [DecidableEq Var] [HasFresh Var] {σ τ : Term Var} (lc : σ.LC) : σ = σ⟦X ↝ τ⟧ := by
   induction lc generalizing X with
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Typing.lean
index d90645505..d55f59a1c 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Typing.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Typing.lean
@@ -22,6 +22,8 @@ The Calculus of Constructions
 
 * [T. Coquand, *An algorithm for type-checking dependent types*][Coquand1996]
 
+* [A. Chargueraud, *The Locally Nameless Representation*][Chargueraud2012]
+
 -/
 
 namespace Cslib
@@ -32,12 +34,28 @@ namespace LambdaCalculus.LocallyNameless.Coc
 
 open Term
 
-/-- β-equivalence. -/
+/-- β-reduction. -/
 inductive BetaEquiv : Term Var → Term Var → Prop
-  /-- Equivalance -/
-  | eq : BetaEquiv (.app (.abs A B) N) (B ^ᵗ N)
-  /-- Congruence -/
-  | cong : BetaEquiv B A → BetaEquiv N M → BetaEquiv (.app B N) (.app A M)
+  /-- β-redex: `(λ A. B) N ⟶ B ^ᵗ N`. -/
+  | red : (abs A B).LC → N.LC → BetaEquiv (.app (.abs A B) N) (B ^ᵗ N)
+  /-- Congruence in the function position of an application. -/
+  | app₁ : t₂.LC → BetaEquiv t₁ t₁' → BetaEquiv (.app t₁ t₂) (.app t₁' t₂)
+  /-- Congruence in the argument position of an application. -/
+  | app₂ : t₁.LC → BetaEquiv t₂ t₂' → BetaEquiv (.app t₁ t₂) (.app t₁ t₂')
+  /-- Congruence in the type annotation of an abstraction. -/
+  | abs₁ : t₂.body → BetaEquiv t₁ t₁' → BetaEquiv (.abs t₁ t₂) (.abs t₁' t₂)
+  /-- Congruence in the body of an abstraction. -/
+  | abs₂ (ρ : Finset Var) :
+      t₁.LC →
+      (∀ x ∉ ρ, BetaEquiv (t₂ ^ᵗ .fvar x) (t₂' ^ᵗ .fvar x)) →
+      BetaEquiv (.abs t₁ t₂) (.abs t₁ t₂')
+  /-- Congruence in the domain of a pi type. -/
+  | pi₁ : t₂.body → BetaEquiv t₁ t₁' → BetaEquiv (.pi t₁ t₂) (.pi t₁' t₂)
+  /-- Congruence in the codomain of a pi type. -/
+  | pi₂ (ρ : Finset Var) :
+      t₁.LC →
+      (∀ x ∉ ρ, BetaEquiv (t₂ ^ᵗ .fvar x) (t₂' ^ᵗ .fvar x)) →
+      BetaEquiv (.pi t₁ t₂) (.pi t₁ t₂')
 
 instance instHasBetaEquivTerm : HasBetaEquiv (Term Var) where
   BetaEquiv := BetaEquiv

From 12c85b0f29789c84e913fcaa9541f10091def37a Mon Sep 17 00:00:00 2001
From: Matt Hunzinger <matt@hunzinger.me>
Date: Wed, 4 Mar 2026 13:02:39 -0500
Subject: [PATCH 16/17] feat: add sort level to Term.type AST

---
 .../Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean | 4 ++--
 .../LambdaCalculus/LocallyNameless/Coc/Opening.lean         | 6 +++---
 .../LambdaCalculus/LocallyNameless/Coc/Typing.lean          | 2 +-
 .../LambdaCalculus/LocallyNameless/Coc/WellFormed.lean      | 2 +-
 4 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean
index 678b1ed48..527291318 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Basic.lean
@@ -42,7 +42,7 @@ inductive Term (Var : Type u) : Type u
   /-- Pi type. -/
   | pi : Term Var → Term Var → Term Var
   /-- Type universe. -/
-  | type : Term Var
+  | type : ℕ → Term Var
 deriving DecidableEq
 
 /-- Free variables. -/
@@ -53,7 +53,7 @@ def Term.fv [DecidableEq Var] : Term Var → Finset Var
   | .app f a => f.fv ∪ a.fv
   | .abs t b => t.fv ∪ b.fv
   | .pi t b => t.fv ∪ b.fv
-  | .type => ∅
+  | .type _ => ∅
 
 abbrev Env (Var : Type u) := Context Var (Term Var)
 
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean
index f6bf29eb6..ed3693029 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Opening.lean
@@ -42,7 +42,7 @@ def openRec (i : ℕ) (s : Term Var) : Term Var → Term Var
   | .app f a => .app (openRec i s f) (openRec i s a)
   | .abs σ t₁ => abs (openRec i s σ) (openRec (i + 1) s t₁)
   | .pi σ t₁ => .pi (openRec i s σ) (openRec (i + 1) s t₁)
-  | .type => .type
+  | .type s => .type s
 
 /-- Variable opening of the closest binding. -/
 @[scoped grind =]
@@ -66,7 +66,7 @@ def subst [DecidableEq Var] (m : Term Var) (x : Var) (r : Term Var) : Term Var :
   | .app f a => .app (f.subst x r) (a.subst x r)
   | .abs t b => .abs (t.subst x r) (b.subst x r)
   | .pi t b => .pi (t.subst x r) (b.subst x r)
-  | .type => .type
+  | .type s => .type s
 
 /-- `Term.subst` is a substitution for λ-terms. Gives access to the notation `m[x := n]`. -/
 instance instHasSubstitutionTerm [DecidableEq Var] :
@@ -93,7 +93,7 @@ inductive LC : Term Var → Prop
   | app : LC t₁ → LC t₂ → LC (app t₁ t₂)
   | abs (L : Finset Var) : t₁.LC → (∀ x ∉ L, LC (t₂ ^ᵗ fvar x)) → LC (abs t₁ t₂)
   | pi (L : Finset Var) : t₁.LC → (∀ x ∉ L, LC (t₂ ^ᵗ fvar x)) → LC (pi t₁ t₂)
-  | type : LC .type
+  | type : LC (.type _)
 
 attribute [scoped grind .] LC.var LC.app LC.type
 
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Typing.lean
index d55f59a1c..655fc7f27 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Typing.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Typing.lean
@@ -77,7 +77,7 @@ inductive Typing [DecidableEq Var] : Env Var → Term Var → Term Var → Prop
       (∀ x ∉ ρ, Typing ({⟨x, A⟩} ∪ Γ) (B ^ᵗ .fvar x) L) →
       Typing Γ (.pi A B) L
   /-- Type universe -/
-  | type : Typing Γ .type .type
+  | type : Typing Γ (.type s) (.type (s + 1))
   /-- β-conversion -/
   | conv : Typing Γ M A → A =β B → Typing Γ M B
 
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/WellFormed.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/WellFormed.lean
index 31d4a8f84..96b5cd4fc 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/WellFormed.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/WellFormed.lean
@@ -44,7 +44,7 @@ inductive Wf : Env Var → Term Var → Prop
       Wf Γ σ →
       (∀ X ∉ L, Wf ({⟨X,σ⟩} ∪ Γ) (τ ^ᵗ fvar X)) →
       Wf Γ (pi σ τ)
-  | type : Wf Γ .type
+  | type : Wf Γ (.type _)
 
 end Term
 

From e69ac78fe495ad2e3db21f867f0ee361e03b6143 Mon Sep 17 00:00:00 2001
From: Matt Hunzinger <matt@hunzinger.me>
Date: Wed, 4 Mar 2026 13:36:10 -0500
Subject: [PATCH 17/17] fix: stronger typing relations in Env.Wf and Typing

---
 .../LocallyNameless/Coc/Typing.lean           | 43 ++++++++++++--
 .../LocallyNameless/Coc/WellFormed.lean       | 58 -------------------
 2 files changed, 37 insertions(+), 64 deletions(-)
 delete mode 100644 Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/WellFormed.lean

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Typing.lean
index 655fc7f27..a1f2f64b7 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Typing.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/Typing.lean
@@ -10,7 +10,7 @@ public import Cslib.Foundations.Data.HasFresh
 public import Cslib.Foundations.Syntax.HasAlphaEquiv
 public import Cslib.Foundations.Syntax.HasBetaEquiv
 public import Cslib.Foundations.Syntax.HasSubstitution
-public import Cslib.Languages.LambdaCalculus.LocallyNameless.Coc.WellFormed
+public import Cslib.Languages.LambdaCalculus.LocallyNameless.Coc.Opening
 
 @[expose] public section
 
@@ -60,8 +60,36 @@ inductive BetaEquiv : Term Var → Term Var → Prop
 instance instHasBetaEquivTerm : HasBetaEquiv (Term Var) where
   BetaEquiv := BetaEquiv
 
+
+variable [DecidableEq Var]
+
+namespace Term
+
+/-- Well-formedness of terms. -/
+inductive Wf : Env Var → Term Var → Prop
+  | var : ⟨x, _⟩ ∈ Γ → Wf Γ (fvar x)
+  | app : Wf Γ f → Wf Γ a → Wf Γ (app f a)
+  | abs (L : Finset Var) :
+      Wf Γ σ →
+      (∀ X ∉ L, Wf ({⟨X,σ⟩} ∪ Γ) (τ ^ᵗ fvar X)) →
+      Wf Γ (abs σ τ)
+  | pi (L : Finset Var) :
+      Wf Γ σ →
+      (∀ X ∉ L, Wf ({⟨X,σ⟩} ∪ Γ) (τ ^ᵗ fvar X)) →
+      Wf Γ (pi σ τ)
+  | type : Wf Γ (type _)
+
+end Term
+
+mutual
+
+/-- An environment is well-formed if it binds each variable exactly once to a well-formed type. -/
+inductive Env.Wf : Env Var → Prop
+  | nil : Env.Wf {}
+  | cons : Env.Wf Γ → Typing Γ τ (.type i) → x ∉ Γ.dom → Env.Wf ({⟨x, τ⟩} ∪ Γ)
+
 /-- Typing judgement -/
-inductive Typing [DecidableEq Var] : Env Var → Term Var → Term Var → Prop
+inductive Typing : Env Var → Term Var → Term Var → Prop
   /-- Variable lookup in Γ -/
   | var : Γ.Wf → ⟨x, A⟩ ∈ Γ → Typing Γ (.fvar x) A
   /-- Function application -/
@@ -73,13 +101,16 @@ inductive Typing [DecidableEq Var] : Env Var → Term Var → Term Var → Prop
       Typing Γ (.abs A N) (.pi A B)
   /-- Pi type -/
   | pi (ρ : Finset Var) :
-      Typing Γ A K →
-      (∀ x ∉ ρ, Typing ({⟨x, A⟩} ∪ Γ) (B ^ᵗ .fvar x) L) →
-      Typing Γ (.pi A B) L
+      Typing Γ A (.type k) →
+      (∀ x ∉ ρ, Typing ({⟨x, A⟩} ∪ Γ) (B ^ᵗ .fvar x) (.type i)) →
+      (i = k ∨ i = 0) →
+      Typing Γ (.pi A B) (.type i)
   /-- Type universe -/
   | type : Typing Γ (.type s) (.type (s + 1))
   /-- β-conversion -/
-  | conv : Typing Γ M A → A =β B → Typing Γ M B
+  | conv : Typing Γ M A → A =β B → Typing Γ B (.type i) → Typing Γ M B
+
+end
 
 end LambdaCalculus.LocallyNameless.Coc
 
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/WellFormed.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/WellFormed.lean
deleted file mode 100644
index 96b5cd4fc..000000000
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Coc/WellFormed.lean
+++ /dev/null
@@ -1,58 +0,0 @@
-/-
-Copyright (c) 2026 Matt Hunzinger. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Matt Hunzinger
--/
-
-module
-
-public import Cslib.Foundations.Data.HasFresh
-public import Cslib.Foundations.Syntax.HasSubstitution
-public import Cslib.Languages.LambdaCalculus.LocallyNameless.Coc.Opening
-
-@[expose] public section
-
-/-! # Calculus of Constructions
-
-The Calculus of Constructions
-
-## References
-
-* [T. Coquand, *An algorithm for type-checking dependent types*][Coquand1996]
-
--/
-
-namespace Cslib
-
-universe u
-
-variable {Var : Type u} [DecidableEq Var]
-
-namespace LambdaCalculus.LocallyNameless.Coc
-
-namespace Term
-
-/-- Well-formedness of terms. -/
-inductive Wf : Env Var → Term Var → Prop
-  | var : ⟨x, _⟩ ∈ Γ → Wf Γ (.fvar x)
-  | app : Wf Γ f → Wf Γ a → Wf Γ (.app f a)
-  | abs (L : Finset Var) :
-      Wf Γ σ →
-      (∀ X ∉ L, Wf ({⟨X,σ⟩} ∪ Γ) (τ ^ᵗ fvar X)) →
-      Wf Γ (abs σ τ)
-  | pi (L : Finset Var) :
-      Wf Γ σ →
-      (∀ X ∉ L, Wf ({⟨X,σ⟩} ∪ Γ) (τ ^ᵗ fvar X)) →
-      Wf Γ (pi σ τ)
-  | type : Wf Γ (.type _)
-
-end Term
-
-/-- An environment is well-formed if it binds each variable exactly once to a well-formed type. -/
-inductive Env.Wf : Env Var → Prop
-  | nil : Wf {}
-  | cons : Wf Γ → Term.Wf Γ τ → x ∉ Γ.dom → Wf ({⟨x, τ⟩} ∪ Γ)
-
-end LambdaCalculus.LocallyNameless.Coc
-
-end Cslib