From 77260763ee1f145de4c38489d349777df53cdf10 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Mon, 21 Jul 2025 20:35:33 -0400
Subject: [PATCH 01/33] first pass at STLC, should consider splitting this file

---
 .../STLC/LocallyNameless/Basic.lean           | 222 ++++++++++++++++++
 1 file changed, 222 insertions(+)
 create mode 100644 Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean

diff --git a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean
new file mode 100644
index 00000000..3db059a8
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean
@@ -0,0 +1,222 @@
+/-
+Copyright (c) 2025 Chris Henson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Henson
+-/
+
+import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Basic
+import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Properties
+import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.FullBetaConfluence
+
+/-! # λ-calculus
+
+The simply typed λ-calculus, with a locally nameless representation of syntax.
+
+## References
+
+* [A. Chargueraud, *The Locally Nameless Representation*] [Chargueraud2012]
+* See also https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/, from which
+  this is partially adapted
+
+-/
+
+universe u
+
+variable {Var : Type u} [DecidableEq Var]
+
+namespace LambdaCalculus.LocallyNameless
+
+/-- Types of the simply typed lambda calculus. -/
+inductive Ty
+/-- A base type, from a typing context. -/
+| base : Ty
+/-- A function type. -/
+| arrow : Ty → Ty → Ty
+
+scoped infixr:70 " ⤳ " => Ty.arrow
+scoped prefix:90 "~ " => Ty.base
+
+/-- A typing context is a list of free variables and corresponding types. -/
+abbrev Ctx (Var : Type u) := List (Var × Ty)
+
+/-- The domain of a context is the finite set of free variables it uses. -/
+@[simp]
+def Ctx.dom : Ctx Var → Finset Var := λ Γ ↦ Γ.map Prod.fst |>.toFinset
+
+/-- A well-formed context. -/
+inductive Ok : Ctx Var → Prop
+| nil : Ok []
+| cons : Ok Γ → x ∉ Γ.dom → Ok ((x,σ) :: Γ)
+
+/-- Context membership is preserved on permuting a context. -/
+theorem Ctx.dom_perm_mem_iff {Γ Δ : Ctx Var} (h : Γ.Perm Δ) {x : Var} : 
+    x ∈ Γ.dom ↔ x ∈ Δ.dom := by
+  induction h <;> aesop
+
+theorem Ctx.dom_perm_nmem {Γ Δ : Ctx Var} (h : Γ.Perm Δ) {x : Var} : 
+    x ∉ Γ.dom → x ∉ Δ.dom := by
+  intros Γ_nmem Δ_mem
+  apply Γ_nmem
+  exact (dom_perm_mem_iff h).mpr Δ_mem
+
+/-- Context well-formedness is preserved on permuting a context. -/
+@[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
+theorem Ok.perm {Γ Δ : Ctx Var} (h : Γ.Perm Δ) : Ok Γ → Ok Δ := by
+  induction h <;> intro Γ_ok
+  case cons perm ih =>
+    cases Γ_ok
+    case cons ok_Γ mem => exact Ok.cons (ih ok_Γ) (Ctx.dom_perm_nmem perm mem)
+  case nil => constructor
+  case trans => simp_all
+  case swap =>
+    cases Γ_ok
+    case cons ok _ =>
+    cases ok
+    case cons ok _ =>
+      constructor
+      constructor
+      all_goals aesop
+
+open Term Ty
+
+/-- An extrinsic typing derivation for locally nameless terms. -/
+@[aesop unsafe [constructors (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]]
+inductive Typing : Ctx Var → Term Var → Ty → Prop
+| var : Ok Γ → (x,σ) ∈ Γ → Typing Γ (fvar x) σ
+| abs (L : Finset Var) : (∀ x ∉ L, Typing ((x,σ) :: Γ) (t ^ fvar x) τ) → Typing Γ t.abs (σ ⤳ τ) 
+| app : Typing Γ t (σ ⤳ τ) → Typing Γ t' σ → Typing Γ (app t t') τ
+
+scoped notation:50 Γ " ⊢ " t " ∶" τ:arg => Typing Γ t τ
+
+variable {Γ Δ Φ : Ctx Var}
+
+/-- Typing is preserved on permuting a context. -/
+theorem Typing.perm : Γ.Perm Δ → Γ ⊢ t ∶ τ → Δ ⊢ t ∶ τ := by 
+  intros _ der
+  revert Δ
+  induction der <;> intros Δ p
+  case app => aesop
+  case var => 
+    have := @p.mem_iff
+    aesop
+  case abs ih => 
+    constructor
+    intros x mem
+    exact ih x mem (by aesop)
+
+open List Finset in
+private lemma weakening_strengthened_eq (eq : Γ_Δ  = Γ ++ Δ) : 
+    Γ_Δ  ⊢ t ∶ τ → Ok (Γ ++ Φ ++ Δ) → (Γ ++ Φ ++ Δ) ⊢ t ∶ τ := by
+  intros h
+  revert Γ Δ Φ
+  induction h <;> intros Γ Δ Φ eq ok_Γ_Φ_Δ
+  case var => aesop
+  case app => aesop
+  case abs σ Γ' τ t xs ext ih =>
+    apply Typing.abs (xs ∪ (Γ ++ Φ ++ Δ).dom)
+    intros x _
+    have h : (x, σ) :: Γ' = (x, σ) :: Γ ++ Δ := by aesop
+    refine @ih x (by aesop) _ _ Φ h ?_
+    constructor <;> aesop
+
+/-- Weakening of a typing derivation with an appended context. -/
+lemma weakening_strengthened : 
+    Γ ++ Δ ⊢ t ∶ τ → Ok (Γ ++ Φ ++ Δ) → (Γ ++ Φ ++ Δ) ⊢ t ∶ τ :=
+  weakening_strengthened_eq rfl
+
+/-- Weakening of a typing derivation by an additional context. -/
+lemma weakening : Γ ⊢ t ∶ T → Ok (Γ ++ Δ) → Γ ++ Δ ⊢ t ∶ T := by
+  intros der ok
+  rw [←List.append_nil (Γ ++ Δ)] at *
+  exact weakening_strengthened (by simp_all) ok
+
+/-- Typing derivations exist only for locally closed terms. -/
+lemma typing_lc : Γ ⊢ t ∶ τ → t.LC := by
+  intros h
+  induction h <;> constructor
+  case abs ih => exact ih
+  all_goals aesop
+
+variable [HasFresh Var]
+
+private lemma typing_subst_strengthened_eq (eq : Φ = Δ ++ (x, σ) :: Γ) :
+    Φ ⊢ t ∶ τ →
+    Γ ⊢ s ∶ σ → 
+    (Δ ++ Γ) ⊢ (t [x := s]) ∶ τ := by
+  intros h
+  revert Γ Δ
+  induction h <;> intros Γ Δ eq der
+  case app => aesop
+  case var x' τ ok mem => 
+    simp only [subst_fvar]
+    rw [eq] at mem
+    rw [eq] at ok
+    cases (Ok.perm (by aesop) ok : Ok ((x, σ) :: Δ ++ Γ))
+    case cons ok_weak _ =>
+    observe perm : (Γ ++ Δ).Perm (Δ ++ Γ)
+    by_cases h : x = x' <;> simp only [h]
+    · rw [show τ = σ by aesop]
+      refine Typing.perm perm (weakening der ?_)
+      exact Ok.perm (id (List.Perm.symm perm)) ok_weak
+    · aesop
+  case abs σ Γ' t T2 xs ih' ih =>
+    apply Typing.abs (xs ∪ {x} ∪ (Δ ++ Γ).dom)
+    intros x _
+    rw [
+      subst_def, 
+      subst_open_var _ _ _ _ _ (typing_lc der),
+      show (x, σ) :: (Δ ++ Γ) = ((x, σ) :: Δ) ++ Γ by aesop
+      ]
+    apply ih 
+    all_goals aesop  
+
+/-- Substitution for a context weakened by a single type between appended contexts. -/
+lemma typing_subst_strengthened :
+  (Δ ++ (z, S) :: Γ) ⊢ t ∶ T →
+  Γ ⊢ s ∶ S → 
+  (Δ ++ Γ) ⊢ (t [z := s]) ∶ T
+  := typing_subst_strengthened_eq rfl
+
+/-- Substitution for a context weakened by a single type. -/
+lemma typing_subst : 
+    (x, σ) :: Γ ⊢ t ∶ τ  → Γ ⊢ s ∶ σ → Γ ⊢ (t [x := s]) ∶ τ := by
+  intros weak der
+  rw [←List.nil_append Γ]
+  exact typing_subst_strengthened weak der
+
+/-- Typing preservation for opening. -/
+@[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
+theorem preservation_opening {xs : Finset Var} :
+  (∀ x ∉ xs, (x, σ) :: Γ ⊢ m ^ fvar x ∶ τ) → 
+  Γ ⊢ n ∶ σ → Γ ⊢ m ^ n ∶ τ
+  := by
+  intros mem der
+  have ⟨fresh, free⟩ := fresh_exists (xs ∪ m.fv)
+  rw [subst_intro fresh n m (by aesop) (typing_lc der)]
+  refine typing_subst (mem fresh (by aesop)) der
+
+/-- Typing preservation. -/
+@[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
+theorem preservation : Γ ⊢ t ∶ τ → (t ⭢βᶠt') → Γ ⊢ t' ∶ τ := by
+  intros der
+  revert t'
+  induction der <;> intros t' step <;> cases step
+  case' abs.abs xs _ _ _ xs' _=> apply Typing.abs (xs ∪ xs')
+  case' app.beta der_l _ _ => cases der_l
+  all_goals aesop
+
+/-- Typing preservation for multiple steps of reduction. -/
+theorem preservation_redex : Γ ⊢ t ∶ T → (t ↠βᶠ t') → Γ ⊢ t' ∶ T := by
+  intros der redex
+  induction redex using Relation.ReflTransGen.trans_induction_on <;> aesop
+
+/-- Typing preservation for confluence. -/
+theorem preservation_confluence :
+    Γ ⊢ a ∶ τ → (a ↠βᶠ b) → (a ↠βᶠ c) → 
+    ∃ d, (b ↠βᶠ d) ∧ (c ↠βᶠ d) ∧ Γ ⊢ d ∶ τ := by
+  intros der ab ac
+  have ⟨d, bd, cd⟩ := confluence_beta ab ac
+  refine ⟨d, bd, cd, preservation_redex der ?_⟩
+  trans
+  exact ab
+  exact bd

From 13ac25948831ddb6957a6b57f21ffb1f7a7ab8c2 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Tue, 22 Jul 2025 10:22:43 -0400
Subject: [PATCH 02/33] structure

---
 .../STLC/LocallyNameless/Basic.lean           | 182 +-----------------
 .../STLC/LocallyNameless/Context.lean         |  65 +++++++
 .../STLC/LocallyNameless/Safety.lean          | 176 +++++++++++++++++
 .../Untyped/LocallyNameless/Basic.lean        |   3 +
 4 files changed, 247 insertions(+), 179 deletions(-)
 create mode 100644 Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Context.lean
 create mode 100644 Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean

diff --git a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean
index 3db059a8..33b1e459 100644
--- a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean
@@ -4,9 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Henson
 -/
 
-import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Basic
-import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Properties
-import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.FullBetaConfluence
+import Cslib.Computability.LambdaCalculus.STLC.LocallyNameless.Context
 
 /-! # λ-calculus
 
@@ -36,187 +34,13 @@ inductive Ty
 scoped infixr:70 " ⤳ " => Ty.arrow
 scoped prefix:90 "~ " => Ty.base
 
-/-- A typing context is a list of free variables and corresponding types. -/
-abbrev Ctx (Var : Type u) := List (Var × Ty)
-
-/-- The domain of a context is the finite set of free variables it uses. -/
-@[simp]
-def Ctx.dom : Ctx Var → Finset Var := λ Γ ↦ Γ.map Prod.fst |>.toFinset
-
-/-- A well-formed context. -/
-inductive Ok : Ctx Var → Prop
-| nil : Ok []
-| cons : Ok Γ → x ∉ Γ.dom → Ok ((x,σ) :: Γ)
-
-/-- Context membership is preserved on permuting a context. -/
-theorem Ctx.dom_perm_mem_iff {Γ Δ : Ctx Var} (h : Γ.Perm Δ) {x : Var} : 
-    x ∈ Γ.dom ↔ x ∈ Δ.dom := by
-  induction h <;> aesop
-
-theorem Ctx.dom_perm_nmem {Γ Δ : Ctx Var} (h : Γ.Perm Δ) {x : Var} : 
-    x ∉ Γ.dom → x ∉ Δ.dom := by
-  intros Γ_nmem Δ_mem
-  apply Γ_nmem
-  exact (dom_perm_mem_iff h).mpr Δ_mem
-
-/-- Context well-formedness is preserved on permuting a context. -/
-@[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
-theorem Ok.perm {Γ Δ : Ctx Var} (h : Γ.Perm Δ) : Ok Γ → Ok Δ := by
-  induction h <;> intro Γ_ok
-  case cons perm ih =>
-    cases Γ_ok
-    case cons ok_Γ mem => exact Ok.cons (ih ok_Γ) (Ctx.dom_perm_nmem perm mem)
-  case nil => constructor
-  case trans => simp_all
-  case swap =>
-    cases Γ_ok
-    case cons ok _ =>
-    cases ok
-    case cons ok _ =>
-      constructor
-      constructor
-      all_goals aesop
-
 open Term Ty
 
 /-- An extrinsic typing derivation for locally nameless terms. -/
 @[aesop unsafe [constructors (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]]
-inductive Typing : Ctx Var → Term Var → Ty → Prop
-| var : Ok Γ → (x,σ) ∈ Γ → Typing Γ (fvar x) σ
+inductive Typing : Ctx Var Ty → Term Var → Ty → Prop
+| var : Γ.Ok → (x,σ) ∈ Γ → Typing Γ (fvar x) σ
 | abs (L : Finset Var) : (∀ x ∉ L, Typing ((x,σ) :: Γ) (t ^ fvar x) τ) → Typing Γ t.abs (σ ⤳ τ) 
 | app : Typing Γ t (σ ⤳ τ) → Typing Γ t' σ → Typing Γ (app t t') τ
 
 scoped notation:50 Γ " ⊢ " t " ∶" τ:arg => Typing Γ t τ
-
-variable {Γ Δ Φ : Ctx Var}
-
-/-- Typing is preserved on permuting a context. -/
-theorem Typing.perm : Γ.Perm Δ → Γ ⊢ t ∶ τ → Δ ⊢ t ∶ τ := by 
-  intros _ der
-  revert Δ
-  induction der <;> intros Δ p
-  case app => aesop
-  case var => 
-    have := @p.mem_iff
-    aesop
-  case abs ih => 
-    constructor
-    intros x mem
-    exact ih x mem (by aesop)
-
-open List Finset in
-private lemma weakening_strengthened_eq (eq : Γ_Δ  = Γ ++ Δ) : 
-    Γ_Δ  ⊢ t ∶ τ → Ok (Γ ++ Φ ++ Δ) → (Γ ++ Φ ++ Δ) ⊢ t ∶ τ := by
-  intros h
-  revert Γ Δ Φ
-  induction h <;> intros Γ Δ Φ eq ok_Γ_Φ_Δ
-  case var => aesop
-  case app => aesop
-  case abs σ Γ' τ t xs ext ih =>
-    apply Typing.abs (xs ∪ (Γ ++ Φ ++ Δ).dom)
-    intros x _
-    have h : (x, σ) :: Γ' = (x, σ) :: Γ ++ Δ := by aesop
-    refine @ih x (by aesop) _ _ Φ h ?_
-    constructor <;> aesop
-
-/-- Weakening of a typing derivation with an appended context. -/
-lemma weakening_strengthened : 
-    Γ ++ Δ ⊢ t ∶ τ → Ok (Γ ++ Φ ++ Δ) → (Γ ++ Φ ++ Δ) ⊢ t ∶ τ :=
-  weakening_strengthened_eq rfl
-
-/-- Weakening of a typing derivation by an additional context. -/
-lemma weakening : Γ ⊢ t ∶ T → Ok (Γ ++ Δ) → Γ ++ Δ ⊢ t ∶ T := by
-  intros der ok
-  rw [←List.append_nil (Γ ++ Δ)] at *
-  exact weakening_strengthened (by simp_all) ok
-
-/-- Typing derivations exist only for locally closed terms. -/
-lemma typing_lc : Γ ⊢ t ∶ τ → t.LC := by
-  intros h
-  induction h <;> constructor
-  case abs ih => exact ih
-  all_goals aesop
-
-variable [HasFresh Var]
-
-private lemma typing_subst_strengthened_eq (eq : Φ = Δ ++ (x, σ) :: Γ) :
-    Φ ⊢ t ∶ τ →
-    Γ ⊢ s ∶ σ → 
-    (Δ ++ Γ) ⊢ (t [x := s]) ∶ τ := by
-  intros h
-  revert Γ Δ
-  induction h <;> intros Γ Δ eq der
-  case app => aesop
-  case var x' τ ok mem => 
-    simp only [subst_fvar]
-    rw [eq] at mem
-    rw [eq] at ok
-    cases (Ok.perm (by aesop) ok : Ok ((x, σ) :: Δ ++ Γ))
-    case cons ok_weak _ =>
-    observe perm : (Γ ++ Δ).Perm (Δ ++ Γ)
-    by_cases h : x = x' <;> simp only [h]
-    · rw [show τ = σ by aesop]
-      refine Typing.perm perm (weakening der ?_)
-      exact Ok.perm (id (List.Perm.symm perm)) ok_weak
-    · aesop
-  case abs σ Γ' t T2 xs ih' ih =>
-    apply Typing.abs (xs ∪ {x} ∪ (Δ ++ Γ).dom)
-    intros x _
-    rw [
-      subst_def, 
-      subst_open_var _ _ _ _ _ (typing_lc der),
-      show (x, σ) :: (Δ ++ Γ) = ((x, σ) :: Δ) ++ Γ by aesop
-      ]
-    apply ih 
-    all_goals aesop  
-
-/-- Substitution for a context weakened by a single type between appended contexts. -/
-lemma typing_subst_strengthened :
-  (Δ ++ (z, S) :: Γ) ⊢ t ∶ T →
-  Γ ⊢ s ∶ S → 
-  (Δ ++ Γ) ⊢ (t [z := s]) ∶ T
-  := typing_subst_strengthened_eq rfl
-
-/-- Substitution for a context weakened by a single type. -/
-lemma typing_subst : 
-    (x, σ) :: Γ ⊢ t ∶ τ  → Γ ⊢ s ∶ σ → Γ ⊢ (t [x := s]) ∶ τ := by
-  intros weak der
-  rw [←List.nil_append Γ]
-  exact typing_subst_strengthened weak der
-
-/-- Typing preservation for opening. -/
-@[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
-theorem preservation_opening {xs : Finset Var} :
-  (∀ x ∉ xs, (x, σ) :: Γ ⊢ m ^ fvar x ∶ τ) → 
-  Γ ⊢ n ∶ σ → Γ ⊢ m ^ n ∶ τ
-  := by
-  intros mem der
-  have ⟨fresh, free⟩ := fresh_exists (xs ∪ m.fv)
-  rw [subst_intro fresh n m (by aesop) (typing_lc der)]
-  refine typing_subst (mem fresh (by aesop)) der
-
-/-- Typing preservation. -/
-@[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
-theorem preservation : Γ ⊢ t ∶ τ → (t ⭢βᶠt') → Γ ⊢ t' ∶ τ := by
-  intros der
-  revert t'
-  induction der <;> intros t' step <;> cases step
-  case' abs.abs xs _ _ _ xs' _=> apply Typing.abs (xs ∪ xs')
-  case' app.beta der_l _ _ => cases der_l
-  all_goals aesop
-
-/-- Typing preservation for multiple steps of reduction. -/
-theorem preservation_redex : Γ ⊢ t ∶ T → (t ↠βᶠ t') → Γ ⊢ t' ∶ T := by
-  intros der redex
-  induction redex using Relation.ReflTransGen.trans_induction_on <;> aesop
-
-/-- Typing preservation for confluence. -/
-theorem preservation_confluence :
-    Γ ⊢ a ∶ τ → (a ↠βᶠ b) → (a ↠βᶠ c) → 
-    ∃ d, (b ↠βᶠ d) ∧ (c ↠βᶠ d) ∧ Γ ⊢ d ∶ τ := by
-  intros der ab ac
-  have ⟨d, bd, cd⟩ := confluence_beta ab ac
-  refine ⟨d, bd, cd, preservation_redex der ?_⟩
-  trans
-  exact ab
-  exact bd
diff --git a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Context.lean b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Context.lean
new file mode 100644
index 00000000..fcc9cf16
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Context.lean
@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2025 Chris Henson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Henson
+-/
+
+import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Basic
+
+/-! # λ-calculus
+
+Contexts as pairs of free variables and types.
+
+-/
+
+universe u v
+
+variable {Var : Type u} {Ty : Type v} [DecidableEq Var]
+
+namespace LambdaCalculus.LocallyNameless
+
+/-- A typing context is a list of free variables and corresponding types. -/
+abbrev Ctx (Var : Type u) (Ty : Type v) := List (Var × Ty)
+
+namespace Ctx
+
+/-- The domain of a context is the finite set of free variables it uses. -/
+@[simp]
+def dom : Ctx Var Ty → Finset Var := λ Γ ↦ Γ.map Prod.fst |>.toFinset
+
+/-- A well-formed context. -/
+inductive Ok : Ctx Var Ty → Prop
+| nil : Ok []
+| cons : Ok Γ → x ∉ Γ.dom → Ok ((x,σ) :: Γ)
+
+variable {Γ Δ : Ctx Var Ty}
+
+/-- Context membership is preserved on permuting a context. -/
+theorem dom_perm_mem_iff (h : Γ.Perm Δ) {x : Var} : 
+    x ∈ Γ.dom ↔ x ∈ Δ.dom := by
+  induction h <;> aesop
+
+/-- Context non-membership is preserved on permuting a context. -/
+theorem dom_perm_nmem (h : Γ.Perm Δ) {x : Var} : 
+    x ∉ Γ.dom → x ∉ Δ.dom := by
+  intros Γ_nmem Δ_mem
+  apply Γ_nmem
+  exact (dom_perm_mem_iff h).mpr Δ_mem
+
+/-- Context well-formedness is preserved on permuting a context. -/
+@[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
+theorem perm (h : Γ.Perm Δ) : Ok Γ → Ok Δ := by
+  induction h <;> intro Γ_ok
+  case cons perm ih =>
+    cases Γ_ok
+    case cons ok_Γ mem => exact Ok.cons (ih ok_Γ) (Ctx.dom_perm_nmem perm mem)
+  case nil => constructor
+  case trans => simp_all
+  case swap =>
+    cases Γ_ok
+    case cons ok _ =>
+    cases ok
+    case cons ok _ =>
+      constructor
+      constructor
+      all_goals aesop
diff --git a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
new file mode 100644
index 00000000..acaad721
--- /dev/null
+++ b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
@@ -0,0 +1,176 @@
+/-
+Copyright (c) 2025 Chris Henson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Henson
+-/
+
+import Cslib.Computability.LambdaCalculus.STLC.LocallyNameless.Basic
+import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Basic
+import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Properties
+import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.FullBetaConfluence
+
+/-! # λ-calculus
+
+Typing preservation of the simply typed λ-calculus, with a locally nameless representation of syntax.
+
+## References
+
+* [A. Chargueraud, *The Locally Nameless Representation*] [Chargueraud2012]
+* See also https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/, from which
+  this is partially adapted
+
+-/
+
+universe u
+
+variable {Var : Type u} [DecidableEq Var]
+
+namespace LambdaCalculus.LocallyNameless.Typing
+
+variable {Γ Δ Φ : Ctx Var Ty}
+
+/-- Typing is preserved on permuting a context. -/
+theorem perm : Γ.Perm Δ → Γ ⊢ t ∶ τ → Δ ⊢ t ∶ τ := by 
+  intros _ der
+  revert Δ
+  induction der <;> intros Δ p
+  case app => aesop
+  case var => 
+    have := @p.mem_iff
+    aesop
+  case abs ih => 
+    constructor
+    intros x mem
+    exact ih x mem (by aesop)
+
+open List Finset in
+private lemma weakening_strengthened_eq (eq : Γ_Δ  = Γ ++ Δ) : 
+    Γ_Δ  ⊢ t ∶ τ → (Γ ++ Φ ++ Δ).Ok → (Γ ++ Φ ++ Δ) ⊢ t ∶ τ := by
+  intros h
+  revert Γ Δ Φ
+  induction h <;> intros Γ Δ Φ eq ok_Γ_Φ_Δ
+  case var => aesop
+  case app => aesop
+  case abs σ Γ' τ t xs ext ih =>
+    apply Typing.abs (xs ∪ (Γ ++ Φ ++ Δ).dom)
+    intros x _
+    have h : (x, σ) :: Γ' = (x, σ) :: Γ ++ Δ := by aesop
+    refine @ih x (by aesop) _ _ Φ h ?_
+    constructor <;> aesop
+
+/-- Weakening of a typing derivation with an appended context. -/
+lemma weakening_strengthened : 
+    Γ ++ Δ ⊢ t ∶ τ → (Γ ++ Φ ++ Δ).Ok → (Γ ++ Φ ++ Δ) ⊢ t ∶ τ :=
+  weakening_strengthened_eq rfl
+
+/-- Weakening of a typing derivation by an additional context. -/
+lemma weakening : Γ ⊢ t ∶ T → (Γ ++ Δ).Ok → Γ ++ Δ ⊢ t ∶ T := by
+  intros der ok
+  rw [←List.append_nil (Γ ++ Δ)] at *
+  exact weakening_strengthened (by simp_all) ok
+
+/-- Typing derivations exist only for locally closed terms. -/
+lemma lc : Γ ⊢ t ∶ τ → t.LC := by
+  intros h
+  induction h <;> constructor
+  case abs ih => exact ih
+  all_goals aesop
+
+variable [HasFresh Var]
+
+open Term
+
+private lemma subst_strengthened_eq (eq : Φ = Δ ++ (x, σ) :: Γ) :
+    Φ ⊢ t ∶ τ →
+    Γ ⊢ s ∶ σ → 
+    (Δ ++ Γ) ⊢ (t [x := s]) ∶ τ := by
+  intros h
+  revert Γ Δ
+  induction h <;> intros Γ Δ eq der
+  case app => aesop
+  case var x' τ ok mem => 
+    simp only [subst_fvar]
+    rw [eq] at mem
+    rw [eq] at ok
+    cases (Ctx.perm (by aesop) ok : @Ctx.Ok Var Ty _ ((x, σ) :: Δ ++ Γ))
+    case cons ok_weak _ =>
+    observe perm : (Γ ++ Δ).Perm (Δ ++ Γ)
+    by_cases h : x = x' <;> simp only [h]
+    · rw [show τ = σ by aesop]
+      refine Typing.perm perm (weakening der ?_)
+      exact Ctx.perm (id (List.Perm.symm perm)) ok_weak
+    · aesop
+  case abs σ Γ' t T2 xs ih' ih =>
+    apply Typing.abs (xs ∪ {x} ∪ (Δ ++ Γ).dom)
+    intros x _
+    rw [
+      subst_def, 
+      subst_open_var _ _ _ _ _ der.lc,
+      show (x, σ) :: (Δ ++ Γ) = ((x, σ) :: Δ) ++ Γ by aesop
+      ]
+    apply ih 
+    all_goals aesop  
+
+/-- Substitution for a context weakened by a single type between appended contexts. -/
+lemma subst_strengthened :
+  (Δ ++ (x, σ) :: Γ) ⊢ t ∶ τ →
+  Γ ⊢ s ∶ σ → 
+  (Δ ++ Γ) ⊢ (t [x := s]) ∶ τ := subst_strengthened_eq rfl
+
+/-- Substitution for a context weakened by a single type. -/
+lemma typing_subst : 
+    (x, σ) :: Γ ⊢ t ∶ τ  → Γ ⊢ s ∶ σ → Γ ⊢ (t [x := s]) ∶ τ := by
+  intros weak der
+  rw [←List.nil_append Γ]
+  exact subst_strengthened weak der
+
+/-- Typing preservation for opening. -/
+@[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
+theorem preservation_opening {xs : Finset Var} :
+  (∀ x ∉ xs, (x, σ) :: Γ ⊢ m ^ fvar x ∶ τ) → 
+  Γ ⊢ n ∶ σ → Γ ⊢ m ^ n ∶ τ
+  := by
+  intros mem der
+  have ⟨fresh, free⟩ := fresh_exists (xs ∪ m.fv)
+  rw [subst_intro fresh n m (by aesop) der.lc]
+  refine typing_subst (mem fresh (by aesop)) der
+
+/-- Typing preservation. -/
+@[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
+theorem preservation : Γ ⊢ t ∶ τ → (t ⭢βᶠt') → Γ ⊢ t' ∶ τ := by
+  intros der
+  revert t'
+  induction der <;> intros t' step <;> cases step
+  case' abs.abs xs _ _ _ xs' _=> apply Typing.abs (xs ∪ xs')
+  case' app.beta der_l _ _ => cases der_l
+  all_goals aesop
+
+/-- Typing preservation for multiple steps of reduction. -/
+theorem preservation_redex : Γ ⊢ t ∶ T → (t ↠βᶠ t') → Γ ⊢ t' ∶ T := by
+  intros der redex
+  induction redex using Relation.ReflTransGen.trans_induction_on <;> aesop
+
+/-- Typing preservation for confluence. -/
+theorem preservation_confluence :
+    Γ ⊢ a ∶ τ → (a ↠βᶠ b) → (a ↠βᶠ c) → 
+    ∃ d, (b ↠βᶠ d) ∧ (c ↠βᶠ d) ∧ Γ ⊢ d ∶ τ := by
+  intros der ab ac
+  have ⟨d, bd, cd⟩ := confluence_beta ab ac
+  refine ⟨d, bd, cd, preservation_redex der ?_⟩
+  trans
+  exact ab
+  exact bd
+
+/-- A typed term either reduces or is a value. -/
+theorem progress : ([] : Ctx Var Ty) ⊢ t ∶ τ → t.Value ∨ ∃ t', t ⭢βᶠ t' := by
+  intros der
+  generalize eq : [] = Γ at der
+  induction der
+  case var => aesop
+  case abs xs mem ih =>
+    left
+    constructor
+    apply Term.LC.abs xs
+    intros _ mem'
+    exact (mem _ mem').lc
+  case app t _ _ t' der_l der_r ih_l ih_r => sorry
diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean
index 646cae50..e8036922 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean
@@ -143,3 +143,6 @@ inductive LC : Term Var → Prop
 | fvar (x)  : LC (fvar x)
 | abs (L : Finset Var) (e : Term Var) : (∀ x : Var, x ∉ L → LC (e ^ fvar x)) → LC (abs e)
 | app {l r} : l.LC → r.LC → LC (app l r)
+
+inductive Value : Term Var → Prop
+| abs (e : Term Var) : e.abs.LC → Value e.abs

From e063572db04772b0a89c160f2ecbd46a0f144c28 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Tue, 22 Jul 2025 10:46:34 -0400
Subject: [PATCH 03/33] progress

---
 .../STLC/LocallyNameless/Safety.lean               | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
index acaad721..dc9dfcb7 100644
--- a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
+++ b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
@@ -161,6 +161,7 @@ theorem preservation_confluence :
   exact ab
   exact bd
 
+omit [HasFresh Var] in
 /-- A typed term either reduces or is a value. -/
 theorem progress : ([] : Ctx Var Ty) ⊢ t ∶ τ → t.Value ∨ ∃ t', t ⭢βᶠ t' := by
   intros der
@@ -173,4 +174,15 @@ theorem progress : ([] : Ctx Var Ty) ⊢ t ∶ τ → t.Value ∨ ∃ t', t ⭢
     apply Term.LC.abs xs
     intros _ mem'
     exact (mem _ mem').lc
-  case app t _ _ t' der_l der_r ih_l ih_r => sorry
+  case app Γ M σ τ N der_l der_r ih_l ih_r => 
+    simp only [eq, forall_const] at *
+    right
+    cases ih_l
+    -- if the lhs is a value, beta reduce the application
+    next val =>
+      cases val
+      next M M_abs_lc => exact ⟨M ^ N, FullBeta.beta M_abs_lc der_r.lc⟩
+    -- otherwise, propogate the step to the lhs of the application
+    next step =>
+      obtain ⟨M', stepM⟩ := step
+      exact ⟨M'.app N, FullBeta.appR der_r.lc stepM⟩ 

From 67ffcc492e1c9f423d1204bc5b03c9e691f443bf Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Tue, 22 Jul 2025 10:58:43 -0400
Subject: [PATCH 04/33] minimize imports

---
 .../LambdaCalculus/STLC/LocallyNameless/Basic.lean            | 1 +
 .../LambdaCalculus/STLC/LocallyNameless/Context.lean          | 4 +++-
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean
index 33b1e459..50da5d04 100644
--- a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean
@@ -5,6 +5,7 @@ Authors: Chris Henson
 -/
 
 import Cslib.Computability.LambdaCalculus.STLC.LocallyNameless.Context
+import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Basic
 
 /-! # λ-calculus
 
diff --git a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Context.lean b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Context.lean
index fcc9cf16..9abf9510 100644
--- a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Context.lean
+++ b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Context.lean
@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Henson
 -/
 
-import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Basic
+import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.AesopRuleset
+import Mathlib.Data.Finset.Defs
+import Mathlib.Data.Finset.Dedup
 
 /-! # λ-calculus
 

From 931a015bf0f84d4bf43d37de8ae08877662dfe16 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Tue, 22 Jul 2025 11:01:59 -0400
Subject: [PATCH 05/33] docs typo

---
 .../LambdaCalculus/Untyped/LocallyNameless/Basic.lean         | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean
index e8036922..9598ab18 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean
@@ -26,9 +26,9 @@ variable {Var : Type u} [HasFresh Var] [DecidableEq Var]
 
 namespace LambdaCalculus.LocallyNameless
 
-/-- Syntax of locally nameless absbda terms, with free variables over `Var`. -/
+/-- Syntax of locally nameless lambda terms, with free variables over `Var`. -/
 inductive Term (Var : Type u)
-/-- Bound variables that appear under a absbda abstraction, using a de-Bruijn index. -/
+/-- Bound variables that appear under a lambda abstraction, using a de-Bruijn index. -/
 | bvar : ℕ → Term Var
 /-- Free variables. -/
 | fvar : Var → Term Var

From a441561b0a771846f34be1437b545658779e573d Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Tue, 22 Jul 2025 11:03:50 -0400
Subject: [PATCH 06/33] docs

---
 .../LambdaCalculus/STLC/LocallyNameless/Basic.lean             | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean
index 50da5d04..87cf0b92 100644
--- a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean
@@ -40,8 +40,11 @@ open Term Ty
 /-- An extrinsic typing derivation for locally nameless terms. -/
 @[aesop unsafe [constructors (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]]
 inductive Typing : Ctx Var Ty → Term Var → Ty → Prop
+/-- Free variables, from a context judgement. -/
 | var : Γ.Ok → (x,σ) ∈ Γ → Typing Γ (fvar x) σ
+/-- Lambda abstraction. -/
 | abs (L : Finset Var) : (∀ x ∉ L, Typing ((x,σ) :: Γ) (t ^ fvar x) τ) → Typing Γ t.abs (σ ⤳ τ) 
+/-- Function application. -/
 | app : Typing Γ t (σ ⤳ τ) → Typing Γ t' σ → Typing Γ (app t t') τ
 
 scoped notation:50 Γ " ⊢ " t " ∶" τ:arg => Typing Γ t τ

From 9507113e4c09bd3176340500124d837f8d89b0a5 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Tue, 22 Jul 2025 11:06:16 -0400
Subject: [PATCH 07/33] docs

---
 .../LambdaCalculus/STLC/LocallyNameless/Safety.lean             | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
index dc9dfcb7..12a74d61 100644
--- a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
+++ b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
@@ -11,7 +11,7 @@ import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.FullBetaConflu
 
 /-! # λ-calculus
 
-Typing preservation of the simply typed λ-calculus, with a locally nameless representation of syntax.
+Typing safety of the simply typed λ-calculus, with a locally nameless representation of syntax.
 
 ## References
 

From 8407b6abad579cc1a2a78c431cc2344aa186b834 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Tue, 22 Jul 2025 11:19:00 -0400
Subject: [PATCH 08/33] remove redundant lemma

---
 .../LambdaCalculus/STLC/LocallyNameless/Context.lean     | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Context.lean b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Context.lean
index 9abf9510..a3679cba 100644
--- a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Context.lean
+++ b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Context.lean
@@ -41,20 +41,13 @@ theorem dom_perm_mem_iff (h : Γ.Perm Δ) {x : Var} :
     x ∈ Γ.dom ↔ x ∈ Δ.dom := by
   induction h <;> aesop
 
-/-- Context non-membership is preserved on permuting a context. -/
-theorem dom_perm_nmem (h : Γ.Perm Δ) {x : Var} : 
-    x ∉ Γ.dom → x ∉ Δ.dom := by
-  intros Γ_nmem Δ_mem
-  apply Γ_nmem
-  exact (dom_perm_mem_iff h).mpr Δ_mem
-
 /-- Context well-formedness is preserved on permuting a context. -/
 @[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
 theorem perm (h : Γ.Perm Δ) : Ok Γ → Ok Δ := by
   induction h <;> intro Γ_ok
   case cons perm ih =>
     cases Γ_ok
-    case cons ok_Γ mem => exact Ok.cons (ih ok_Γ) (Ctx.dom_perm_nmem perm mem)
+    case cons ok_Γ nmem => exact Ok.cons (ih ok_Γ) $ (dom_perm_mem_iff perm).not.mp nmem
   case nil => constructor
   case trans => simp_all
   case swap =>

From 1465525dec3f553357f9f7ab4494fb7a40b6c858 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Tue, 22 Jul 2025 11:22:40 -0400
Subject: [PATCH 09/33] style

---
 .../LambdaCalculus/STLC/LocallyNameless/Safety.lean           | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
index 12a74d61..5f086778 100644
--- a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
+++ b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
@@ -64,7 +64,7 @@ lemma weakening_strengthened :
   weakening_strengthened_eq rfl
 
 /-- Weakening of a typing derivation by an additional context. -/
-lemma weakening : Γ ⊢ t ∶ T → (Γ ++ Δ).Ok → Γ ++ Δ ⊢ t ∶ T := by
+lemma weakening : Γ ⊢ t ∶ τ → (Γ ++ Δ).Ok → Γ ++ Δ ⊢ t ∶ τ := by
   intros der ok
   rw [←List.append_nil (Γ ++ Δ)] at *
   exact weakening_strengthened (by simp_all) ok
@@ -146,7 +146,7 @@ theorem preservation : Γ ⊢ t ∶ τ → (t ⭢βᶠt') → Γ ⊢ t' ∶ τ :
   all_goals aesop
 
 /-- Typing preservation for multiple steps of reduction. -/
-theorem preservation_redex : Γ ⊢ t ∶ T → (t ↠βᶠ t') → Γ ⊢ t' ∶ T := by
+theorem preservation_redex : Γ ⊢ t ∶ τ → (t ↠βᶠ t') → Γ ⊢ t' ∶ τ := by
   intros der redex
   induction redex using Relation.ReflTransGen.trans_induction_on <;> aesop
 

From 14191cd8fcda3f295b42f93fbfd866c1b3709f19 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Tue, 22 Jul 2025 11:36:01 -0400
Subject: [PATCH 10/33] style

---
 .../LambdaCalculus/Untyped/LocallyNameless/Basic.lean           | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean
index 9598ab18..c7a7edab 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean
@@ -145,4 +145,4 @@ inductive LC : Term Var → Prop
 | app {l r} : l.LC → r.LC → LC (app l r)
 
 inductive Value : Term Var → Prop
-| abs (e : Term Var) : e.abs.LC → Value e.abs
+| abs (e : Term Var) : e.abs.LC → e.abs.Value

From ac6a0fda23944817b82cfe6a897ea4aed3a7db43 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Wed, 23 Jul 2025 16:10:30 -0400
Subject: [PATCH 11/33] eliminate private lemma

---
 .../STLC/LocallyNameless/Safety.lean               | 14 +++++---------
 1 file changed, 5 insertions(+), 9 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
index 5f086778..6d5dc3b3 100644
--- a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
+++ b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
@@ -43,9 +43,10 @@ theorem perm : Γ.Perm Δ → Γ ⊢ t ∶ τ → Δ ⊢ t ∶ τ := by
     intros x mem
     exact ih x mem (by aesop)
 
-open List Finset in
-private lemma weakening_strengthened_eq (eq : Γ_Δ  = Γ ++ Δ) : 
-    Γ_Δ  ⊢ t ∶ τ → (Γ ++ Φ ++ Δ).Ok → (Γ ++ Φ ++ Δ) ⊢ t ∶ τ := by
+/-- Weakening of a typing derivation with an appended context. -/
+lemma weakening_strengthened : 
+    Γ ++ Δ ⊢ t ∶ τ → (Γ ++ Φ ++ Δ).Ok → (Γ ++ Φ ++ Δ) ⊢ t ∶ τ := by
+  generalize eq : Γ ++ Δ = Γ_Δ
   intros h
   revert Γ Δ Φ
   induction h <;> intros Γ Δ Φ eq ok_Γ_Φ_Δ
@@ -54,15 +55,10 @@ private lemma weakening_strengthened_eq (eq : Γ_Δ  = Γ ++ Δ) :
   case abs σ Γ' τ t xs ext ih =>
     apply Typing.abs (xs ∪ (Γ ++ Φ ++ Δ).dom)
     intros x _
-    have h : (x, σ) :: Γ' = (x, σ) :: Γ ++ Δ := by aesop
+    have h : (x, σ) :: Γ ++ Δ = (x, σ) :: Γ' := by aesop
     refine @ih x (by aesop) _ _ Φ h ?_
     constructor <;> aesop
 
-/-- Weakening of a typing derivation with an appended context. -/
-lemma weakening_strengthened : 
-    Γ ++ Δ ⊢ t ∶ τ → (Γ ++ Φ ++ Δ).Ok → (Γ ++ Φ ++ Δ) ⊢ t ∶ τ :=
-  weakening_strengthened_eq rfl
-
 /-- Weakening of a typing derivation by an additional context. -/
 lemma weakening : Γ ⊢ t ∶ τ → (Γ ++ Δ).Ok → Γ ++ Δ ⊢ t ∶ τ := by
   intros der ok

From a67d1c1531ff384a5e60b5c990955b0c95783c3f Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Wed, 23 Jul 2025 16:14:28 -0400
Subject: [PATCH 12/33] eliminate private lemma

---
 .../STLC/LocallyNameless/Safety.lean             | 16 ++++++----------
 1 file changed, 6 insertions(+), 10 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
index 6d5dc3b3..768f8e82 100644
--- a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
+++ b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
@@ -76,18 +76,20 @@ variable [HasFresh Var]
 
 open Term
 
-private lemma subst_strengthened_eq (eq : Φ = Δ ++ (x, σ) :: Γ) :
-    Φ ⊢ t ∶ τ →
+/-- Substitution for a context weakened by a single type between appended contexts. -/
+lemma subst_strengthened :
+    (Δ ++ (x, σ) :: Γ) ⊢ t ∶ τ →
     Γ ⊢ s ∶ σ → 
     (Δ ++ Γ) ⊢ (t [x := s]) ∶ τ := by
+  generalize  eq : Δ ++ (x, σ) :: Γ = Φ
   intros h
   revert Γ Δ
   induction h <;> intros Γ Δ eq der
   case app => aesop
   case var x' τ ok mem => 
     simp only [subst_fvar]
-    rw [eq] at mem
-    rw [eq] at ok
+    rw [←eq] at mem
+    rw [←eq] at ok
     cases (Ctx.perm (by aesop) ok : @Ctx.Ok Var Ty _ ((x, σ) :: Δ ++ Γ))
     case cons ok_weak _ =>
     observe perm : (Γ ++ Δ).Perm (Δ ++ Γ)
@@ -107,12 +109,6 @@ private lemma subst_strengthened_eq (eq : Φ = Δ ++ (x, σ) :: Γ) :
     apply ih 
     all_goals aesop  
 
-/-- Substitution for a context weakened by a single type between appended contexts. -/
-lemma subst_strengthened :
-  (Δ ++ (x, σ) :: Γ) ⊢ t ∶ τ →
-  Γ ⊢ s ∶ σ → 
-  (Δ ++ Γ) ⊢ (t [x := s]) ∶ τ := subst_strengthened_eq rfl
-
 /-- Substitution for a context weakened by a single type. -/
 lemma typing_subst : 
     (x, σ) :: Γ ⊢ t ∶ τ  → Γ ⊢ s ∶ σ → Γ ⊢ (t [x := s]) ∶ τ := by

From 2ded228841bbbb5a409c8fcc8ebcc6eb9511052f Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Wed, 23 Jul 2025 16:29:09 -0400
Subject: [PATCH 13/33] scope safety theorems

---
 .../STLC/LocallyNameless/Safety.lean           | 18 ++++++++++++++----
 1 file changed, 14 insertions(+), 4 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
index 768f8e82..e1116f2b 100644
--- a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
+++ b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
@@ -127,7 +127,15 @@ theorem preservation_opening {xs : Finset Var} :
   rw [subst_intro fresh n m (by aesop) der.lc]
   refine typing_subst (mem fresh (by aesop)) der
 
-/-- Typing preservation. -/
+end Typing
+
+namespace Term.FullBeta
+
+open Typing
+
+variable [HasFresh Var] {Γ : Ctx Var Ty}
+
+/-- Typing preservation for full beta reduction. -/
 @[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
 theorem preservation : Γ ⊢ t ∶ τ → (t ⭢βᶠt') → Γ ⊢ t' ∶ τ := by
   intros der
@@ -137,12 +145,12 @@ theorem preservation : Γ ⊢ t ∶ τ → (t ⭢βᶠt') → Γ ⊢ t' ∶ τ :
   case' app.beta der_l _ _ => cases der_l
   all_goals aesop
 
-/-- Typing preservation for multiple steps of reduction. -/
+/-- Typing preservation for multiple steps of full beta reduction. -/
 theorem preservation_redex : Γ ⊢ t ∶ τ → (t ↠βᶠ t') → Γ ⊢ t' ∶ τ := by
   intros der redex
   induction redex using Relation.ReflTransGen.trans_induction_on <;> aesop
 
-/-- Typing preservation for confluence. -/
+/-- Typing preservation for full beta confluence. -/
 theorem preservation_confluence :
     Γ ⊢ a ∶ τ → (a ↠βᶠ b) → (a ↠βᶠ c) → 
     ∃ d, (b ↠βᶠ d) ∧ (c ↠βᶠ d) ∧ Γ ⊢ d ∶ τ := by
@@ -154,7 +162,7 @@ theorem preservation_confluence :
   exact bd
 
 omit [HasFresh Var] in
-/-- A typed term either reduces or is a value. -/
+/-- A typed term either full beta reduces or is a value. -/
 theorem progress : ([] : Ctx Var Ty) ⊢ t ∶ τ → t.Value ∨ ∃ t', t ⭢βᶠ t' := by
   intros der
   generalize eq : [] = Γ at der
@@ -178,3 +186,5 @@ theorem progress : ([] : Ctx Var Ty) ⊢ t ∶ τ → t.Value ∨ ∃ t', t ⭢
     next step =>
       obtain ⟨M', stepM⟩ := step
       exact ⟨M'.app N, FullBeta.appR der_r.lc stepM⟩ 
+
+end Term.FullBeta

From 7c38c408a3a26947d55e7698021803e5de1292ab Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Wed, 23 Jul 2025 16:34:29 -0400
Subject: [PATCH 14/33] STLC namespace

---
 .../LambdaCalculus/STLC/LocallyNameless/Basic.lean          | 2 +-
 .../LambdaCalculus/STLC/LocallyNameless/Context.lean        | 2 +-
 .../LambdaCalculus/STLC/LocallyNameless/Safety.lean         | 6 +++---
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean
index 87cf0b92..b26dca4d 100644
--- a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean
@@ -23,7 +23,7 @@ universe u
 
 variable {Var : Type u} [DecidableEq Var]
 
-namespace LambdaCalculus.LocallyNameless
+namespace LambdaCalculus.LocallyNameless.STLC
 
 /-- Types of the simply typed lambda calculus. -/
 inductive Ty
diff --git a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Context.lean b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Context.lean
index a3679cba..c92e3d0d 100644
--- a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Context.lean
+++ b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Context.lean
@@ -18,7 +18,7 @@ universe u v
 
 variable {Var : Type u} {Ty : Type v} [DecidableEq Var]
 
-namespace LambdaCalculus.LocallyNameless
+namespace LambdaCalculus.LocallyNameless.STLC
 
 /-- A typing context is a list of free variables and corresponding types. -/
 abbrev Ctx (Var : Type u) (Ty : Type v) := List (Var × Ty)
diff --git a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
index e1116f2b..aab13d0e 100644
--- a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
+++ b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
@@ -25,7 +25,7 @@ universe u
 
 variable {Var : Type u} [DecidableEq Var]
 
-namespace LambdaCalculus.LocallyNameless.Typing
+namespace LambdaCalculus.LocallyNameless.STLC.Typing
 
 variable {Γ Δ Φ : Ctx Var Ty}
 
@@ -127,11 +127,11 @@ theorem preservation_opening {xs : Finset Var} :
   rw [subst_intro fresh n m (by aesop) der.lc]
   refine typing_subst (mem fresh (by aesop)) der
 
-end Typing
+end STLC.Typing
 
 namespace Term.FullBeta
 
-open Typing
+open STLC Typing
 
 variable [HasFresh Var] {Γ : Ctx Var Ty}
 

From 194e11d401dd71397b75db2c0a8c4defc4548c81 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Wed, 23 Jul 2025 17:26:24 -0400
Subject: [PATCH 15/33] restructure for clarity

---
 .../STLC/LocallyNameless/Basic.lean           | 104 ++++++++++++-
 .../STLC/LocallyNameless/Safety.lean          | 143 +++---------------
 2 files changed, 125 insertions(+), 122 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean
index b26dca4d..362675be 100644
--- a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean
@@ -5,7 +5,7 @@ Authors: Chris Henson
 -/
 
 import Cslib.Computability.LambdaCalculus.STLC.LocallyNameless.Context
-import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Basic
+import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Properties
 
 /-! # λ-calculus
 
@@ -48,3 +48,105 @@ inductive Typing : Ctx Var Ty → Term Var → Ty → Prop
 | app : Typing Γ t (σ ⤳ τ) → Typing Γ t' σ → Typing Γ (app t t') τ
 
 scoped notation:50 Γ " ⊢ " t " ∶" τ:arg => Typing Γ t τ
+
+namespace Typing
+
+variable {Γ Δ Φ : Ctx Var Ty}
+
+/-- Typing is preserved on permuting a context. -/
+theorem perm : Γ.Perm Δ → Γ ⊢ t ∶ τ → Δ ⊢ t ∶ τ := by 
+  intros _ der
+  revert Δ
+  induction der <;> intros Δ p
+  case app => aesop
+  case var => 
+    have := @p.mem_iff
+    aesop
+  case abs ih => 
+    constructor
+    intros x mem
+    exact ih x mem (by aesop)
+
+/-- Weakening of a typing derivation with an appended context. -/
+lemma weakening_strengthened : 
+    Γ ++ Δ ⊢ t ∶ τ → (Γ ++ Φ ++ Δ).Ok → (Γ ++ Φ ++ Δ) ⊢ t ∶ τ := by
+  generalize eq : Γ ++ Δ = Γ_Δ
+  intros h
+  revert Γ Δ Φ
+  induction h <;> intros Γ Δ Φ eq ok_Γ_Φ_Δ
+  case var => aesop
+  case app => aesop
+  case abs σ Γ' τ t xs ext ih =>
+    apply Typing.abs (xs ∪ (Γ ++ Φ ++ Δ).dom)
+    intros x _
+    have h : (x, σ) :: Γ ++ Δ = (x, σ) :: Γ' := by aesop
+    refine @ih x (by aesop) _ _ Φ h ?_
+    constructor <;> aesop
+
+/-- Weakening of a typing derivation by an additional context. -/
+lemma weakening : Γ ⊢ t ∶ τ → (Γ ++ Δ).Ok → Γ ++ Δ ⊢ t ∶ τ := by
+  intros der ok
+  rw [←List.append_nil (Γ ++ Δ)] at *
+  exact weakening_strengthened (by simp_all) ok
+
+/-- Typing derivations exist only for locally closed terms. -/
+lemma lc : Γ ⊢ t ∶ τ → t.LC := by
+  intros h
+  induction h <;> constructor
+  case abs ih => exact ih
+  all_goals aesop
+
+variable [HasFresh Var]
+
+open Term
+
+/-- Substitution for a context weakened by a single type between appended contexts. -/
+lemma subst_strengthened :
+    (Δ ++ (x, σ) :: Γ) ⊢ t ∶ τ →
+    Γ ⊢ s ∶ σ → 
+    (Δ ++ Γ) ⊢ (t [x := s]) ∶ τ := by
+  generalize  eq : Δ ++ (x, σ) :: Γ = Φ
+  intros h
+  revert Γ Δ
+  induction h <;> intros Γ Δ eq der
+  case app => aesop
+  case var x' τ ok mem => 
+    simp only [subst_fvar]
+    rw [←eq] at mem
+    rw [←eq] at ok
+    cases (Ctx.perm (by aesop) ok : @Ctx.Ok Var Ty _ ((x, σ) :: Δ ++ Γ))
+    case cons ok_weak _ =>
+    observe perm : (Γ ++ Δ).Perm (Δ ++ Γ)
+    by_cases h : x = x' <;> simp only [h]
+    · rw [show τ = σ by aesop]
+      refine Typing.perm perm (weakening der ?_)
+      exact Ctx.perm (id (List.Perm.symm perm)) ok_weak
+    · aesop
+  case abs σ Γ' t T2 xs ih' ih =>
+    apply Typing.abs (xs ∪ {x} ∪ (Δ ++ Γ).dom)
+    intros x _
+    rw [
+      subst_def, 
+      subst_open_var _ _ _ _ _ der.lc,
+      show (x, σ) :: (Δ ++ Γ) = ((x, σ) :: Δ) ++ Γ by aesop
+      ]
+    apply ih 
+    all_goals aesop  
+
+/-- Substitution for a context weakened by a single type. -/
+lemma typing_subst : 
+    (x, σ) :: Γ ⊢ t ∶ τ  → Γ ⊢ s ∶ σ → Γ ⊢ (t [x := s]) ∶ τ := by
+  intros weak der
+  rw [←List.nil_append Γ]
+  exact subst_strengthened weak der
+
+/-- Typing preservation for opening. -/
+@[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
+theorem preservation_opening {xs : Finset Var} :
+  (∀ x ∉ xs, (x, σ) :: Γ ⊢ m ^ fvar x ∶ τ) → 
+  Γ ⊢ n ∶ σ → Γ ⊢ m ^ n ∶ τ
+  := by
+  intros mem der
+  have ⟨fresh, free⟩ := fresh_exists (xs ∪ m.fv)
+  rw [subst_intro fresh n m (by aesop) der.lc]
+  refine typing_subst (mem fresh (by aesop)) der
diff --git a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
index aab13d0e..8a695d95 100644
--- a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
+++ b/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
@@ -11,7 +11,8 @@ import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.FullBetaConflu
 
 /-! # λ-calculus
 
-Typing safety of the simply typed λ-calculus, with a locally nameless representation of syntax.
+Type safety of the simply typed λ-calculus, with a locally nameless representation of syntax.
+Theorems in this file are namespaced by their respective reductions.
 
 ## References
 
@@ -23,118 +24,34 @@ Typing safety of the simply typed λ-calculus, with a locally nameless represent
 
 universe u
 
-variable {Var : Type u} [DecidableEq Var]
+namespace LambdaCalculus.LocallyNameless
 
-namespace LambdaCalculus.LocallyNameless.STLC.Typing
+open STLC Typing
 
-variable {Γ Δ Φ : Ctx Var Ty}
+variable {Var : Type u} [DecidableEq Var] {R : Term Var → Term Var → Prop}
 
-/-- Typing is preserved on permuting a context. -/
-theorem perm : Γ.Perm Δ → Γ ⊢ t ∶ τ → Δ ⊢ t ∶ τ := by 
-  intros _ der
-  revert Δ
-  induction der <;> intros Δ p
-  case app => aesop
-  case var => 
-    have := @p.mem_iff
-    aesop
-  case abs ih => 
-    constructor
-    intros x mem
-    exact ih x mem (by aesop)
-
-/-- Weakening of a typing derivation with an appended context. -/
-lemma weakening_strengthened : 
-    Γ ++ Δ ⊢ t ∶ τ → (Γ ++ Φ ++ Δ).Ok → (Γ ++ Φ ++ Δ) ⊢ t ∶ τ := by
-  generalize eq : Γ ++ Δ = Γ_Δ
-  intros h
-  revert Γ Δ Φ
-  induction h <;> intros Γ Δ Φ eq ok_Γ_Φ_Δ
-  case var => aesop
-  case app => aesop
-  case abs σ Γ' τ t xs ext ih =>
-    apply Typing.abs (xs ∪ (Γ ++ Φ ++ Δ).dom)
-    intros x _
-    have h : (x, σ) :: Γ ++ Δ = (x, σ) :: Γ' := by aesop
-    refine @ih x (by aesop) _ _ Φ h ?_
-    constructor <;> aesop
-
-/-- Weakening of a typing derivation by an additional context. -/
-lemma weakening : Γ ⊢ t ∶ τ → (Γ ++ Δ).Ok → Γ ++ Δ ⊢ t ∶ τ := by
-  intros der ok
-  rw [←List.append_nil (Γ ++ Δ)] at *
-  exact weakening_strengthened (by simp_all) ok
-
-/-- Typing derivations exist only for locally closed terms. -/
-lemma lc : Γ ⊢ t ∶ τ → t.LC := by
-  intros h
-  induction h <;> constructor
-  case abs ih => exact ih
-  all_goals aesop
+def preserves (R : Term Var → Term Var → Prop) := ∀ {Γ t t' τ}, Γ ⊢ t ∶ τ → R t t' → Γ ⊢ t' ∶ τ
 
-variable [HasFresh Var]
-
-open Term
-
-/-- Substitution for a context weakened by a single type between appended contexts. -/
-lemma subst_strengthened :
-    (Δ ++ (x, σ) :: Γ) ⊢ t ∶ τ →
-    Γ ⊢ s ∶ σ → 
-    (Δ ++ Γ) ⊢ (t [x := s]) ∶ τ := by
-  generalize  eq : Δ ++ (x, σ) :: Γ = Φ
-  intros h
-  revert Γ Δ
-  induction h <;> intros Γ Δ eq der
-  case app => aesop
-  case var x' τ ok mem => 
-    simp only [subst_fvar]
-    rw [←eq] at mem
-    rw [←eq] at ok
-    cases (Ctx.perm (by aesop) ok : @Ctx.Ok Var Ty _ ((x, σ) :: Δ ++ Γ))
-    case cons ok_weak _ =>
-    observe perm : (Γ ++ Δ).Perm (Δ ++ Γ)
-    by_cases h : x = x' <;> simp only [h]
-    · rw [show τ = σ by aesop]
-      refine Typing.perm perm (weakening der ?_)
-      exact Ctx.perm (id (List.Perm.symm perm)) ok_weak
-    · aesop
-  case abs σ Γ' t T2 xs ih' ih =>
-    apply Typing.abs (xs ∪ {x} ∪ (Δ ++ Γ).dom)
-    intros x _
-    rw [
-      subst_def, 
-      subst_open_var _ _ _ _ _ der.lc,
-      show (x, σ) :: (Δ ++ Γ) = ((x, σ) :: Δ) ++ Γ by aesop
-      ]
-    apply ih 
-    all_goals aesop  
-
-/-- Substitution for a context weakened by a single type. -/
-lemma typing_subst : 
-    (x, σ) :: Γ ⊢ t ∶ τ  → Γ ⊢ s ∶ σ → Γ ⊢ (t [x := s]) ∶ τ := by
-  intros weak der
-  rw [←List.nil_append Γ]
-  exact subst_strengthened weak der
-
-/-- Typing preservation for opening. -/
+/-- If a reduction preserves types, so does its reflexive transitive closure. -/
 @[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
-theorem preservation_opening {xs : Finset Var} :
-  (∀ x ∉ xs, (x, σ) :: Γ ⊢ m ^ fvar x ∶ τ) → 
-  Γ ⊢ n ∶ σ → Γ ⊢ m ^ n ∶ τ
-  := by
-  intros mem der
-  have ⟨fresh, free⟩ := fresh_exists (xs ∪ m.fv)
-  rw [subst_intro fresh n m (by aesop) der.lc]
-  refine typing_subst (mem fresh (by aesop)) der
-
-end STLC.Typing
+theorem preservation_redex : preserves R → preserves (Relation.ReflTransGen R) := by
+  intros _ _ _ _ _ _ redex
+  induction redex <;> aesop
+
+open Relation in
+/-- Confluence preserves type preservation. -/
+theorem preservation_confluence : 
+    Confluence R → preserves R → Γ ⊢ a ∶ τ → 
+    (ReflTransGen R) a b → (ReflTransGen R) a c →
+    ∃ d, (ReflTransGen R) b d ∧ (ReflTransGen R) c d ∧ Γ ⊢ d ∶ τ := by
+  intros con p der ab ac
+  have ⟨d, bd, cd⟩ := con ab ac
+  exact ⟨d, bd, cd, preservation_redex p der (ab.trans bd)⟩
+ 
+variable [HasFresh Var] {Γ : Ctx Var Ty}
 
 namespace Term.FullBeta
 
-open STLC Typing
-
-variable [HasFresh Var] {Γ : Ctx Var Ty}
-
 /-- Typing preservation for full beta reduction. -/
 @[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
 theorem preservation : Γ ⊢ t ∶ τ → (t ⭢βᶠt') → Γ ⊢ t' ∶ τ := by
@@ -145,22 +62,6 @@ theorem preservation : Γ ⊢ t ∶ τ → (t ⭢βᶠt') → Γ ⊢ t' ∶ τ :
   case' app.beta der_l _ _ => cases der_l
   all_goals aesop
 
-/-- Typing preservation for multiple steps of full beta reduction. -/
-theorem preservation_redex : Γ ⊢ t ∶ τ → (t ↠βᶠ t') → Γ ⊢ t' ∶ τ := by
-  intros der redex
-  induction redex using Relation.ReflTransGen.trans_induction_on <;> aesop
-
-/-- Typing preservation for full beta confluence. -/
-theorem preservation_confluence :
-    Γ ⊢ a ∶ τ → (a ↠βᶠ b) → (a ↠βᶠ c) → 
-    ∃ d, (b ↠βᶠ d) ∧ (c ↠βᶠ d) ∧ Γ ⊢ d ∶ τ := by
-  intros der ab ac
-  have ⟨d, bd, cd⟩ := confluence_beta ab ac
-  refine ⟨d, bd, cd, preservation_redex der ?_⟩
-  trans
-  exact ab
-  exact bd
-
 omit [HasFresh Var] in
 /-- A typed term either full beta reduces or is a value. -/
 theorem progress : ([] : Ctx Var Ty) ⊢ t ∶ τ → t.Value ∨ ∃ t', t ⭢βᶠ t' := by

From 89d81e89ff09568ed9ca67b35563f8b30977d394 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Wed, 23 Jul 2025 17:42:54 -0400
Subject: [PATCH 16/33] reverse directory structure

---
 .../LocallyNameless => LocallyNameless/STLC}/Basic.lean   | 4 ++--
 .../LocallyNameless => LocallyNameless/STLC}/Context.lean | 2 +-
 .../LocallyNameless => LocallyNameless/STLC}/Safety.lean  | 8 ++++----
 .../Untyped}/AesopRuleset.lean                            | 0
 .../Untyped}/Basic.lean                                   | 2 +-
 .../Untyped}/FullBeta.lean                                | 4 ++--
 .../Untyped}/FullBetaConfluence.lean                      | 6 +++---
 .../Untyped}/Properties.lean                              | 2 +-
 .../{Untyped/Named => Named/Untyped}/Basic.lean           | 0
 CslibTests/LambdaCalculus.lean                            | 2 +-
 10 files changed, 15 insertions(+), 15 deletions(-)
 rename Cslib/Computability/LambdaCalculus/{STLC/LocallyNameless => LocallyNameless/STLC}/Basic.lean (97%)
 rename Cslib/Computability/LambdaCalculus/{STLC/LocallyNameless => LocallyNameless/STLC}/Context.lean (95%)
 rename Cslib/Computability/LambdaCalculus/{STLC/LocallyNameless => LocallyNameless/STLC}/Safety.lean (90%)
 rename Cslib/Computability/LambdaCalculus/{Untyped/LocallyNameless => LocallyNameless/Untyped}/AesopRuleset.lean (100%)
 rename Cslib/Computability/LambdaCalculus/{Untyped/LocallyNameless => LocallyNameless/Untyped}/Basic.lean (98%)
 rename Cslib/Computability/LambdaCalculus/{Untyped/LocallyNameless => LocallyNameless/Untyped}/FullBeta.lean (96%)
 rename Cslib/Computability/LambdaCalculus/{Untyped/LocallyNameless => LocallyNameless/Untyped}/FullBetaConfluence.lean (97%)
 rename Cslib/Computability/LambdaCalculus/{Untyped/LocallyNameless => LocallyNameless/Untyped}/Properties.lean (98%)
 rename Cslib/Computability/LambdaCalculus/{Untyped/Named => Named/Untyped}/Basic.lean (100%)

diff --git a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Basic.lean
similarity index 97%
rename from Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean
rename to Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Basic.lean
index 362675be..6c70e4ef 100644
--- a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Basic.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Henson
 -/
 
-import Cslib.Computability.LambdaCalculus.STLC.LocallyNameless.Context
-import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Properties
+import Cslib.Computability.LambdaCalculus.LocallyNameless.STLC.Context
+import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.Properties
 
 /-! # λ-calculus
 
diff --git a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Context.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Context.lean
similarity index 95%
rename from Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Context.lean
rename to Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Context.lean
index c92e3d0d..b84da8d6 100644
--- a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Context.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Context.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Henson
 -/
 
-import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.AesopRuleset
+import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.AesopRuleset
 import Mathlib.Data.Finset.Defs
 import Mathlib.Data.Finset.Dedup
 
diff --git a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Safety.lean
similarity index 90%
rename from Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
rename to Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Safety.lean
index 8a695d95..5749acd7 100644
--- a/Cslib/Computability/LambdaCalculus/STLC/LocallyNameless/Safety.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Safety.lean
@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Henson
 -/
 
-import Cslib.Computability.LambdaCalculus.STLC.LocallyNameless.Basic
-import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Basic
-import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Properties
-import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.FullBetaConfluence
+import Cslib.Computability.LambdaCalculus.LocallyNameless.STLC.Basic
+import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.Basic
+import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.Properties
+import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
 
 /-! # λ-calculus
 
diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/AesopRuleset.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/AesopRuleset.lean
similarity index 100%
rename from Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/AesopRuleset.lean
rename to Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/AesopRuleset.lean
diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/Basic.lean
similarity index 98%
rename from Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean
rename to Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/Basic.lean
index c7a7edab..88a82fd6 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/Basic.lean
@@ -6,7 +6,7 @@ Authors: Chris Henson
 
 import Cslib.Data.HasFresh
 import Cslib.Syntax.HasSubstitution
-import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.AesopRuleset
+import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.AesopRuleset
 
 /-! # λ-calculus
 
diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBeta.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
similarity index 96%
rename from Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBeta.lean
rename to Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
index 35bc61bc..e1572151 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBeta.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Henson
 -/
 
-import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Basic
-import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Properties
+import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.Basic
+import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.Properties
 import Cslib.Semantics.ReductionSystem.Basic
 
 /-! # β-reduction for the λ-calculus
diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean
similarity index 97%
rename from Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean
rename to Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean
index 9c64387c..ac9c00f1 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/FullBetaConfluence.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean
@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Henson
 -/
 
-import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Basic
-import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Properties
-import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.FullBeta
+import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.Basic
+import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.Properties
+import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.FullBeta
 import Cslib.Data.Relation
 
 /-! # β-confluence for the λ-calculus -/
diff --git a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Properties.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/Properties.lean
similarity index 98%
rename from Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Properties.lean
rename to Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/Properties.lean
index 69fbb9b2..f9fb146e 100644
--- a/Cslib/Computability/LambdaCalculus/Untyped/LocallyNameless/Properties.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Untyped/Properties.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Henson
 -/
 
-import Cslib.Computability.LambdaCalculus.Untyped.LocallyNameless.Basic
+import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.Basic
 
 universe u
 
diff --git a/Cslib/Computability/LambdaCalculus/Untyped/Named/Basic.lean b/Cslib/Computability/LambdaCalculus/Named/Untyped/Basic.lean
similarity index 100%
rename from Cslib/Computability/LambdaCalculus/Untyped/Named/Basic.lean
rename to Cslib/Computability/LambdaCalculus/Named/Untyped/Basic.lean
diff --git a/CslibTests/LambdaCalculus.lean b/CslibTests/LambdaCalculus.lean
index abc6dfb8..c92d97a8 100644
--- a/CslibTests/LambdaCalculus.lean
+++ b/CslibTests/LambdaCalculus.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
-import Cslib.Computability.LambdaCalculus.Untyped.Named.Basic
+import Cslib.Computability.LambdaCalculus.Named.Untyped.Basic
 
 open LambdaCalculus.Named
 open LambdaCalculus.Named.Term

From fcd57641f3b5384c2dee220cfffe82a0699590e6 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Fri, 25 Jul 2025 03:33:55 -0400
Subject: [PATCH 17/33] paramaterize Ty base a base type

---
 .../LocallyNameless/STLC/Basic.lean             | 16 ++++++++--------
 .../LocallyNameless/STLC/Safety.lean            | 17 +++++++++--------
 2 files changed, 17 insertions(+), 16 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Basic.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Basic.lean
index 6c70e4ef..07a298ec 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Basic.lean
@@ -19,18 +19,18 @@ The simply typed λ-calculus, with a locally nameless representation of syntax.
 
 -/
 
-universe u
+universe u v
 
-variable {Var : Type u} [DecidableEq Var]
+variable {Var : Type u} {Base : Type v} [DecidableEq Var]
 
 namespace LambdaCalculus.LocallyNameless.STLC
 
 /-- Types of the simply typed lambda calculus. -/
-inductive Ty
+inductive Ty (Base : Type v)
 /-- A base type, from a typing context. -/
-| base : Ty
+| base : Base → Ty Base
 /-- A function type. -/
-| arrow : Ty → Ty → Ty
+| arrow : Ty Base → Ty Base → Ty Base
 
 scoped infixr:70 " ⤳ " => Ty.arrow
 scoped prefix:90 "~ " => Ty.base
@@ -39,7 +39,7 @@ open Term Ty
 
 /-- An extrinsic typing derivation for locally nameless terms. -/
 @[aesop unsafe [constructors (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]]
-inductive Typing : Ctx Var Ty → Term Var → Ty → Prop
+inductive Typing : Ctx Var (Ty Base) → Term Var → Ty Base → Prop
 /-- Free variables, from a context judgement. -/
 | var : Γ.Ok → (x,σ) ∈ Γ → Typing Γ (fvar x) σ
 /-- Lambda abstraction. -/
@@ -51,7 +51,7 @@ scoped notation:50 Γ " ⊢ " t " ∶" τ:arg => Typing Γ t τ
 
 namespace Typing
 
-variable {Γ Δ Φ : Ctx Var Ty}
+variable {Γ Δ Φ : Ctx Var (Ty Base)}
 
 /-- Typing is preserved on permuting a context. -/
 theorem perm : Γ.Perm Δ → Γ ⊢ t ∶ τ → Δ ⊢ t ∶ τ := by 
@@ -114,7 +114,7 @@ lemma subst_strengthened :
     simp only [subst_fvar]
     rw [←eq] at mem
     rw [←eq] at ok
-    cases (Ctx.perm (by aesop) ok : @Ctx.Ok Var Ty _ ((x, σ) :: Δ ++ Γ))
+    cases (Ctx.perm (by aesop) ok : @Ctx.Ok Var (Ty Base) _ ((x, σ) :: Δ ++ Γ))
     case cons ok_weak _ =>
     observe perm : (Γ ++ Δ).Perm (Δ ++ Γ)
     by_cases h : x = x' <;> simp only [h]
diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Safety.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Safety.lean
index 5749acd7..021a2fdd 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Safety.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Safety.lean
@@ -22,33 +22,34 @@ Theorems in this file are namespaced by their respective reductions.
 
 -/
 
-universe u
+universe u v
 
 namespace LambdaCalculus.LocallyNameless
 
 open STLC Typing
 
-variable {Var : Type u} [DecidableEq Var] {R : Term Var → Term Var → Prop}
+variable {Var : Type u} {Base : Type v} [DecidableEq Var] {R : Term Var → Term Var → Prop}
 
-def preserves (R : Term Var → Term Var → Prop) := ∀ {Γ t t' τ}, Γ ⊢ t ∶ τ → R t t' → Γ ⊢ t' ∶ τ
+def preserves (R : Term Var → Term Var → Prop) (Base : Type v) := 
+  ∀ {Γ t t'} {τ : Ty Base}, Γ ⊢ t ∶ τ → R t t' → Γ ⊢ t' ∶ τ
 
 /-- If a reduction preserves types, so does its reflexive transitive closure. -/
 @[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
-theorem preservation_redex : preserves R → preserves (Relation.ReflTransGen R) := by
+theorem preservation_redex : preserves R Base → preserves (Relation.ReflTransGen R) Base := by
   intros _ _ _ _ _ _ redex
   induction redex <;> aesop
 
 open Relation in
 /-- Confluence preserves type preservation. -/
-theorem preservation_confluence : 
-    Confluence R → preserves R → Γ ⊢ a ∶ τ → 
+theorem preservation_confluence {τ : Ty Base} : 
+    Confluence R → preserves R Base → Γ ⊢ a ∶ τ → 
     (ReflTransGen R) a b → (ReflTransGen R) a c →
     ∃ d, (ReflTransGen R) b d ∧ (ReflTransGen R) c d ∧ Γ ⊢ d ∶ τ := by
   intros con p der ab ac
   have ⟨d, bd, cd⟩ := con ab ac
   exact ⟨d, bd, cd, preservation_redex p der (ab.trans bd)⟩
  
-variable [HasFresh Var] {Γ : Ctx Var Ty}
+variable [HasFresh Var] {Γ : Ctx Var (Ty Base)}
 
 namespace Term.FullBeta
 
@@ -64,7 +65,7 @@ theorem preservation : Γ ⊢ t ∶ τ → (t ⭢βᶠt') → Γ ⊢ t' ∶ τ :
 
 omit [HasFresh Var] in
 /-- A typed term either full beta reduces or is a value. -/
-theorem progress : ([] : Ctx Var Ty) ⊢ t ∶ τ → t.Value ∨ ∃ t', t ⭢βᶠ t' := by
+theorem progress : ([] : Ctx Var (Ty Base)) ⊢ t ∶ τ → t.Value ∨ ∃ t', t ⭢βᶠ t' := by
   intros der
   generalize eq : [] = Γ at der
   induction der

From 02281846bc8c69bd2638e407992c8261d647ece8 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Fri, 25 Jul 2025 04:40:03 -0400
Subject: [PATCH 18/33] rm unused notation

---
 .../Computability/LambdaCalculus/LocallyNameless/STLC/Basic.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Basic.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Basic.lean
index 07a298ec..ceb5e2c3 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Basic.lean
@@ -33,7 +33,6 @@ inductive Ty (Base : Type v)
 | arrow : Ty Base → Ty Base → Ty Base
 
 scoped infixr:70 " ⤳ " => Ty.arrow
-scoped prefix:90 "~ " => Ty.base
 
 open Term Ty
 

From ba67f03bc842a6700ca88a9ebe3d616bd9d0a08c Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Fri, 25 Jul 2025 04:46:16 -0400
Subject: [PATCH 19/33] naming convention

---
 .../LambdaCalculus/LocallyNameless/{STLC => Stlc}/Basic.lean  | 4 ++--
 .../LocallyNameless/{STLC => Stlc}/Context.lean               | 2 +-
 .../LambdaCalculus/LocallyNameless/{STLC => Stlc}/Safety.lean | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)
 rename Cslib/Computability/LambdaCalculus/LocallyNameless/{STLC => Stlc}/Basic.lean (97%)
 rename Cslib/Computability/LambdaCalculus/LocallyNameless/{STLC => Stlc}/Context.lean (97%)
 rename Cslib/Computability/LambdaCalculus/LocallyNameless/{STLC => Stlc}/Safety.lean (97%)

diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Basic.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
similarity index 97%
rename from Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Basic.lean
rename to Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
index ceb5e2c3..ca41eb1d 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Henson
 -/
 
-import Cslib.Computability.LambdaCalculus.LocallyNameless.STLC.Context
+import Cslib.Computability.LambdaCalculus.LocallyNameless.Stlc.Context
 import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.Properties
 
 /-! # λ-calculus
@@ -23,7 +23,7 @@ universe u v
 
 variable {Var : Type u} {Base : Type v} [DecidableEq Var]
 
-namespace LambdaCalculus.LocallyNameless.STLC
+namespace LambdaCalculus.LocallyNameless.Stlc
 
 /-- Types of the simply typed lambda calculus. -/
 inductive Ty (Base : Type v)
diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Context.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
similarity index 97%
rename from Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Context.lean
rename to Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
index b84da8d6..a40a4842 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Context.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
@@ -18,7 +18,7 @@ universe u v
 
 variable {Var : Type u} {Ty : Type v} [DecidableEq Var]
 
-namespace LambdaCalculus.LocallyNameless.STLC
+namespace LambdaCalculus.LocallyNameless.Stlc
 
 /-- A typing context is a list of free variables and corresponding types. -/
 abbrev Ctx (Var : Type u) (Ty : Type v) := List (Var × Ty)
diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Safety.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
similarity index 97%
rename from Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Safety.lean
rename to Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
index 021a2fdd..37a9a7e5 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/STLC/Safety.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Henson
 -/
 
-import Cslib.Computability.LambdaCalculus.LocallyNameless.STLC.Basic
+import Cslib.Computability.LambdaCalculus.LocallyNameless.Stlc.Basic
 import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.Basic
 import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.Properties
 import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.FullBetaConfluence
@@ -26,7 +26,7 @@ universe u v
 
 namespace LambdaCalculus.LocallyNameless
 
-open STLC Typing
+open Stlc Typing
 
 variable {Var : Type u} {Base : Type v} [DecidableEq Var] {R : Term Var → Term Var → Prop}
 

From 5f475a9d109805f8ee79c7ba3f40b17fe0dc7c64 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Fri, 25 Jul 2025 05:00:48 -0400
Subject: [PATCH 20/33] nicer speelling of Ctx.dom

---
 .../LambdaCalculus/LocallyNameless/Stlc/Context.lean            | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
index a40a4842..4d8b0635 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
@@ -27,7 +27,7 @@ namespace Ctx
 
 /-- The domain of a context is the finite set of free variables it uses. -/
 @[simp]
-def dom : Ctx Var Ty → Finset Var := λ Γ ↦ Γ.map Prod.fst |>.toFinset
+def dom : Ctx Var Ty → Finset Var := List.toFinset ∘ List.map Prod.fst
 
 /-- A well-formed context. -/
 inductive Ok : Ctx Var Ty → Prop

From d358fd03d0813633922fe6f8e48fcc9494c5c1df Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Fri, 25 Jul 2025 05:03:13 -0400
Subject: [PATCH 21/33] rm terminal refine

---
 .../LambdaCalculus/LocallyNameless/Stlc/Basic.lean              | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
index ca41eb1d..4e6a0145 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
@@ -148,4 +148,4 @@ theorem preservation_opening {xs : Finset Var} :
   intros mem der
   have ⟨fresh, free⟩ := fresh_exists (xs ∪ m.fv)
   rw [subst_intro fresh n m (by aesop) der.lc]
-  refine typing_subst (mem fresh (by aesop)) der
+  exact typing_subst (mem fresh (by aesop)) der

From 016238ea3087384e61bb8e903a2efd296f073789 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Fri, 25 Jul 2025 05:05:58 -0400
Subject: [PATCH 22/33] style

---
 .../LambdaCalculus/LocallyNameless/Stlc/Context.lean            | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
index 4d8b0635..de944314 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
@@ -47,7 +47,7 @@ theorem perm (h : Γ.Perm Δ) : Ok Γ → Ok Δ := by
   induction h <;> intro Γ_ok
   case cons perm ih =>
     cases Γ_ok
-    case cons ok_Γ nmem => exact Ok.cons (ih ok_Γ) $ (dom_perm_mem_iff perm).not.mp nmem
+    case cons ok_Γ nmem => exact (ih ok_Γ).cons $ (dom_perm_mem_iff perm).not.mp nmem
   case nil => constructor
   case trans => simp_all
   case swap =>

From 2bc822fe0ae843230ce08643cb413fd90ba6f1c4 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Mon, 28 Jul 2025 13:14:42 -0400
Subject: [PATCH 23/33] use Data.List.Sigma

---
 .../LocallyNameless/Stlc/Basic.lean           | 38 ++++++++++++-------
 .../LocallyNameless/Stlc/Context.lean         | 33 +++++++---------
 .../LocallyNameless/Stlc/Safety.lean          |  6 +--
 3 files changed, 41 insertions(+), 36 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
index 4e6a0145..1ba96754 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
@@ -40,9 +40,9 @@ open Term Ty
 @[aesop unsafe [constructors (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]]
 inductive Typing : Ctx Var (Ty Base) → Term Var → Ty Base → Prop
 /-- Free variables, from a context judgement. -/
-| var : Γ.Ok → (x,σ) ∈ Γ → Typing Γ (fvar x) σ
+| var : Γ.Ok → ⟨x,σ⟩ ∈ Γ → Typing Γ (fvar x) σ
 /-- Lambda abstraction. -/
-| abs (L : Finset Var) : (∀ x ∉ L, Typing ((x,σ) :: Γ) (t ^ fvar x) τ) → Typing Γ t.abs (σ ⤳ τ) 
+| abs (L : Finset Var) : (∀ x ∉ L, Typing (⟨x,σ⟩ :: Γ) (t ^ fvar x) τ) → Typing Γ t.abs (σ ⤳ τ) 
 /-- Function application. -/
 | app : Typing Γ t (σ ⤳ τ) → Typing Γ t' σ → Typing Γ (app t t') τ
 
@@ -52,6 +52,7 @@ namespace Typing
 
 variable {Γ Δ Φ : Ctx Var (Ty Base)}
 
+omit [DecidableEq Var] in
 /-- Typing is preserved on permuting a context. -/
 theorem perm : Γ.Perm Δ → Γ ⊢ t ∶ τ → Δ ⊢ t ∶ τ := by 
   intros _ der
@@ -78,9 +79,8 @@ lemma weakening_strengthened :
   case abs σ Γ' τ t xs ext ih =>
     apply Typing.abs (xs ∪ (Γ ++ Φ ++ Δ).dom)
     intros x _
-    have h : (x, σ) :: Γ ++ Δ = (x, σ) :: Γ' := by aesop
-    refine @ih x (by aesop) _ _ Φ h ?_
-    constructor <;> aesop
+    have h : ⟨x, σ⟩ :: Γ ++ Δ = ⟨x, σ⟩ :: Γ' := by aesop
+    refine @ih x ?_ _ _ Φ h ?_ <;> aesop
 
 /-- Weakening of a typing derivation by an additional context. -/
 lemma weakening : Γ ⊢ t ∶ τ → (Γ ++ Δ).Ok → Γ ++ Δ ⊢ t ∶ τ := by
@@ -88,6 +88,7 @@ lemma weakening : Γ ⊢ t ∶ τ → (Γ ++ Δ).Ok → Γ ++ Δ ⊢ t ∶ τ :=
   rw [←List.append_nil (Γ ++ Δ)] at *
   exact weakening_strengthened (by simp_all) ok
 
+omit [DecidableEq Var] in
 /-- Typing derivations exist only for locally closed terms. -/
 lemma lc : Γ ⊢ t ∶ τ → t.LC := by
   intros h
@@ -101,10 +102,10 @@ open Term
 
 /-- Substitution for a context weakened by a single type between appended contexts. -/
 lemma subst_strengthened :
-    (Δ ++ (x, σ) :: Γ) ⊢ t ∶ τ →
+    (Δ ++ ⟨x, σ⟩ :: Γ) ⊢ t ∶ τ →
     Γ ⊢ s ∶ σ → 
     (Δ ++ Γ) ⊢ (t [x := s]) ∶ τ := by
-  generalize  eq : Δ ++ (x, σ) :: Γ = Φ
+  generalize  eq : Δ ++ ⟨x, σ⟩ :: Γ = Φ
   intros h
   revert Γ Δ
   induction h <;> intros Γ Δ eq der
@@ -113,28 +114,39 @@ lemma subst_strengthened :
     simp only [subst_fvar]
     rw [←eq] at mem
     rw [←eq] at ok
-    cases (Ctx.perm (by aesop) ok : @Ctx.Ok Var (Ty Base) _ ((x, σ) :: Δ ++ Γ))
+    cases (Ctx.perm (by aesop) ok : Ctx.Ok (⟨x, σ⟩ :: Δ ++ Γ))
     case cons ok_weak _ =>
     observe perm : (Γ ++ Δ).Perm (Δ ++ Γ)
     by_cases h : x = x' <;> simp only [h]
-    · rw [show τ = σ by aesop]
+    case neg => aesop
+    case pos nmem =>
+      subst h eq
+      have nmem_Γ : ∀ γ, ⟨x, γ⟩ ∉ Γ := by
+        intros γ _
+        exact nmem x (List.mem_keys.mpr ⟨γ, by aesop⟩) rfl
+      have nmem_Δ : ∀ γ, ⟨x, γ⟩ ∉ Δ := by
+        intros γ _
+        exact nmem x (List.mem_keys.mpr ⟨γ, by aesop⟩) rfl
+      have eq' : τ = σ := by
+        simp only [List.mem_append, List.mem_cons, Sigma.mk.injEq, heq_eq_eq] at mem
+        match mem with | _ => aesop
+      rw [eq']
       refine Typing.perm perm (weakening der ?_)
       exact Ctx.perm (id (List.Perm.symm perm)) ok_weak
-    · aesop
   case abs σ Γ' t T2 xs ih' ih =>
     apply Typing.abs (xs ∪ {x} ∪ (Δ ++ Γ).dom)
     intros x _
     rw [
       subst_def, 
       subst_open_var _ _ _ _ _ der.lc,
-      show (x, σ) :: (Δ ++ Γ) = ((x, σ) :: Δ) ++ Γ by aesop
+      show ⟨x, σ⟩ :: (Δ ++ Γ) = (⟨x, σ⟩ :: Δ) ++ Γ by aesop
       ]
     apply ih 
     all_goals aesop  
 
 /-- Substitution for a context weakened by a single type. -/
 lemma typing_subst : 
-    (x, σ) :: Γ ⊢ t ∶ τ  → Γ ⊢ s ∶ σ → Γ ⊢ (t [x := s]) ∶ τ := by
+    ⟨x, σ⟩ :: Γ ⊢ t ∶ τ  → Γ ⊢ s ∶ σ → Γ ⊢ (t [x := s]) ∶ τ := by
   intros weak der
   rw [←List.nil_append Γ]
   exact subst_strengthened weak der
@@ -142,7 +154,7 @@ lemma typing_subst :
 /-- Typing preservation for opening. -/
 @[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
 theorem preservation_opening {xs : Finset Var} :
-  (∀ x ∉ xs, (x, σ) :: Γ ⊢ m ^ fvar x ∶ τ) → 
+  (∀ x ∉ xs, ⟨x, σ⟩ :: Γ ⊢ m ^ fvar x ∶ τ) → 
   Γ ⊢ n ∶ σ → Γ ⊢ m ^ n ∶ τ
   := by
   intros mem der
diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
index de944314..af619570 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
@@ -7,6 +7,7 @@ Authors: Chris Henson
 import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.AesopRuleset
 import Mathlib.Data.Finset.Defs
 import Mathlib.Data.Finset.Dedup
+import Mathlib.Data.List.Sigma
 
 /-! # λ-calculus
 
@@ -21,18 +22,16 @@ variable {Var : Type u} {Ty : Type v} [DecidableEq Var]
 namespace LambdaCalculus.LocallyNameless.Stlc
 
 /-- A typing context is a list of free variables and corresponding types. -/
-abbrev Ctx (Var : Type u) (Ty : Type v) := List (Var × Ty)
+abbrev Ctx (Var : Type u) (Ty : Type v) := List ((_ : Var) × Ty)
 
 namespace Ctx
 
 /-- The domain of a context is the finite set of free variables it uses. -/
 @[simp]
-def dom : Ctx Var Ty → Finset Var := List.toFinset ∘ List.map Prod.fst
+def dom : Ctx Var Ty → Finset Var := List.toFinset ∘ List.keys
 
 /-- A well-formed context. -/
-inductive Ok : Ctx Var Ty → Prop
-| nil : Ok []
-| cons : Ok Γ → x ∉ Γ.dom → Ok ((x,σ) :: Γ)
+abbrev Ok : Ctx Var Ty → Prop := List.NodupKeys
 
 variable {Γ Δ : Ctx Var Ty}
 
@@ -41,20 +40,14 @@ theorem dom_perm_mem_iff (h : Γ.Perm Δ) {x : Var} :
     x ∈ Γ.dom ↔ x ∈ Δ.dom := by
   induction h <;> aesop
 
+omit [DecidableEq Var] in
 /-- Context well-formedness is preserved on permuting a context. -/
 @[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
-theorem perm (h : Γ.Perm Δ) : Ok Γ → Ok Δ := by
-  induction h <;> intro Γ_ok
-  case cons perm ih =>
-    cases Γ_ok
-    case cons ok_Γ nmem => exact (ih ok_Γ).cons $ (dom_perm_mem_iff perm).not.mp nmem
-  case nil => constructor
-  case trans => simp_all
-  case swap =>
-    cases Γ_ok
-    case cons ok _ =>
-    cases ok
-    case cons ok _ =>
-      constructor
-      constructor
-      all_goals aesop
+theorem perm (h : Γ.Perm Δ) : Ok Γ → Ok Δ := (List.perm_nodupKeys h).mp
+
+omit [DecidableEq Var] in
+@[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
+theorem strengthen : (Δ ++ ⟨x, σ⟩ :: Γ).Ok → (Δ ++ Γ).Ok := by
+  intros ok
+  have sl : List.Sublist (Δ ++ Γ) (Δ ++ ⟨x, σ⟩ :: Γ) := by simp
+  exact List.NodupKeys.sublist sl ok
diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
index 37a9a7e5..e38ff4ef 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
@@ -28,7 +28,7 @@ namespace LambdaCalculus.LocallyNameless
 
 open Stlc Typing
 
-variable {Var : Type u} {Base : Type v} [DecidableEq Var] {R : Term Var → Term Var → Prop}
+variable {Var : Type u} {Base : Type v} {R : Term Var → Term Var → Prop}
 
 def preserves (R : Term Var → Term Var → Prop) (Base : Type v) := 
   ∀ {Γ t t'} {τ : Ty Base}, Γ ⊢ t ∶ τ → R t t' → Γ ⊢ t' ∶ τ
@@ -49,7 +49,7 @@ theorem preservation_confluence {τ : Ty Base} :
   have ⟨d, bd, cd⟩ := con ab ac
   exact ⟨d, bd, cd, preservation_redex p der (ab.trans bd)⟩
  
-variable [HasFresh Var] {Γ : Ctx Var (Ty Base)}
+variable [HasFresh Var] [DecidableEq Var] {Γ : Ctx Var (Ty Base)}
 
 namespace Term.FullBeta
 
@@ -63,7 +63,7 @@ theorem preservation : Γ ⊢ t ∶ τ → (t ⭢βᶠt') → Γ ⊢ t' ∶ τ :
   case' app.beta der_l _ _ => cases der_l
   all_goals aesop
 
-omit [HasFresh Var] in
+omit [HasFresh Var] [DecidableEq Var] in
 /-- A typed term either full beta reduces or is a value. -/
 theorem progress : ([] : Ctx Var (Ty Base)) ⊢ t ∶ τ → t.Value ∨ ∃ t', t ⭢βᶠ t' := by
   intros der

From bb502ec2a880ee4e5e94df836d1869d60e2dc2b0 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Mon, 28 Jul 2025 13:39:10 -0400
Subject: [PATCH 24/33] use HasWellFormed notation

---
 .../LambdaCalculus/LocallyNameless/Stlc/Basic.lean   | 12 +++++++-----
 .../LambdaCalculus/LocallyNameless/Stlc/Context.lean |  8 ++++++--
 2 files changed, 13 insertions(+), 7 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
index 1ba96754..bf14a9ad 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
@@ -40,7 +40,7 @@ open Term Ty
 @[aesop unsafe [constructors (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]]
 inductive Typing : Ctx Var (Ty Base) → Term Var → Ty Base → Prop
 /-- Free variables, from a context judgement. -/
-| var : Γ.Ok → ⟨x,σ⟩ ∈ Γ → Typing Γ (fvar x) σ
+| var : Γ ✓ → ⟨x,σ⟩ ∈ Γ → Typing Γ (fvar x) σ
 /-- Lambda abstraction. -/
 | abs (L : Finset Var) : (∀ x ∉ L, Typing (⟨x,σ⟩ :: Γ) (t ^ fvar x) τ) → Typing Γ t.abs (σ ⤳ τ) 
 /-- Function application. -/
@@ -69,7 +69,7 @@ theorem perm : Γ.Perm Δ → Γ ⊢ t ∶ τ → Δ ⊢ t ∶ τ := by
 
 /-- Weakening of a typing derivation with an appended context. -/
 lemma weakening_strengthened : 
-    Γ ++ Δ ⊢ t ∶ τ → (Γ ++ Φ ++ Δ).Ok → (Γ ++ Φ ++ Δ) ⊢ t ∶ τ := by
+    Γ ++ Δ ⊢ t ∶ τ → (Γ ++ Φ ++ Δ) ✓ → (Γ ++ Φ ++ Δ) ⊢ t ∶ τ := by
   generalize eq : Γ ++ Δ = Γ_Δ
   intros h
   revert Γ Δ Φ
@@ -80,10 +80,12 @@ lemma weakening_strengthened :
     apply Typing.abs (xs ∪ (Γ ++ Φ ++ Δ).dom)
     intros x _
     have h : ⟨x, σ⟩ :: Γ ++ Δ = ⟨x, σ⟩ :: Γ' := by aesop
-    refine @ih x ?_ _ _ Φ h ?_ <;> aesop
+    refine @ih x (by aesop) _ _ Φ h ?_
+    simp only [HasWellFormed.wf]
+    aesop
 
 /-- Weakening of a typing derivation by an additional context. -/
-lemma weakening : Γ ⊢ t ∶ τ → (Γ ++ Δ).Ok → Γ ++ Δ ⊢ t ∶ τ := by
+lemma weakening : Γ ⊢ t ∶ τ → (Γ ++ Δ) ✓ → Γ ++ Δ ⊢ t ∶ τ := by
   intros der ok
   rw [←List.append_nil (Γ ++ Δ)] at *
   exact weakening_strengthened (by simp_all) ok
@@ -114,7 +116,7 @@ lemma subst_strengthened :
     simp only [subst_fvar]
     rw [←eq] at mem
     rw [←eq] at ok
-    cases (Ctx.perm (by aesop) ok : Ctx.Ok (⟨x, σ⟩ :: Δ ++ Γ))
+    cases (Ctx.perm (by aesop) ok : (⟨x, σ⟩ :: Δ ++ Γ) ✓)
     case cons ok_weak _ =>
     observe perm : (Γ ++ Δ).Perm (Δ ++ Γ)
     by_cases h : x = x' <;> simp only [h]
diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
index af619570..9826e5d8 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
@@ -5,6 +5,7 @@ Authors: Chris Henson
 -/
 
 import Cslib.Computability.LambdaCalculus.LocallyNameless.Untyped.AesopRuleset
+import Cslib.Syntax.HasWellFormed
 import Mathlib.Data.Finset.Defs
 import Mathlib.Data.Finset.Dedup
 import Mathlib.Data.List.Sigma
@@ -33,6 +34,9 @@ def dom : Ctx Var Ty → Finset Var := List.toFinset ∘ List.keys
 /-- A well-formed context. -/
 abbrev Ok : Ctx Var Ty → Prop := List.NodupKeys
 
+instance : HasWellFormed (Ctx Var Ty) :=
+  ⟨Ok⟩
+
 variable {Γ Δ : Ctx Var Ty}
 
 /-- Context membership is preserved on permuting a context. -/
@@ -43,11 +47,11 @@ theorem dom_perm_mem_iff (h : Γ.Perm Δ) {x : Var} :
 omit [DecidableEq Var] in
 /-- Context well-formedness is preserved on permuting a context. -/
 @[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
-theorem perm (h : Γ.Perm Δ) : Ok Γ → Ok Δ := (List.perm_nodupKeys h).mp
+theorem perm (h : Γ.Perm Δ) : Γ ✓ → Δ ✓ := (List.perm_nodupKeys h).mp
 
 omit [DecidableEq Var] in
 @[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
-theorem strengthen : (Δ ++ ⟨x, σ⟩ :: Γ).Ok → (Δ ++ Γ).Ok := by
+theorem strengthen : (Δ ++ ⟨x, σ⟩ :: Γ) ✓ → (Δ ++ Γ) ✓ := by
   intros ok
   have sl : List.Sublist (Δ ++ Γ) (Δ ++ ⟨x, σ⟩ :: Γ) := by simp
   exact List.NodupKeys.sublist sl ok

From 0a5b708ba043934a886bd970b687d92686ba1298 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Mon, 28 Jul 2025 13:48:31 -0400
Subject: [PATCH 25/33] Ctx -> Context

---
 .../LambdaCalculus/LocallyNameless/Stlc/Basic.lean   |  8 ++++----
 .../LambdaCalculus/LocallyNameless/Stlc/Context.lean | 12 ++++++------
 .../LambdaCalculus/LocallyNameless/Stlc/Safety.lean  |  4 ++--
 3 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
index bf14a9ad..2a0534ab 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
@@ -38,7 +38,7 @@ open Term Ty
 
 /-- An extrinsic typing derivation for locally nameless terms. -/
 @[aesop unsafe [constructors (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]]
-inductive Typing : Ctx Var (Ty Base) → Term Var → Ty Base → Prop
+inductive Typing : Context Var (Ty Base) → Term Var → Ty Base → Prop
 /-- Free variables, from a context judgement. -/
 | var : Γ ✓ → ⟨x,σ⟩ ∈ Γ → Typing Γ (fvar x) σ
 /-- Lambda abstraction. -/
@@ -50,7 +50,7 @@ scoped notation:50 Γ " ⊢ " t " ∶" τ:arg => Typing Γ t τ
 
 namespace Typing
 
-variable {Γ Δ Φ : Ctx Var (Ty Base)}
+variable {Γ Δ Φ : Context Var (Ty Base)}
 
 omit [DecidableEq Var] in
 /-- Typing is preserved on permuting a context. -/
@@ -116,7 +116,7 @@ lemma subst_strengthened :
     simp only [subst_fvar]
     rw [←eq] at mem
     rw [←eq] at ok
-    cases (Ctx.perm (by aesop) ok : (⟨x, σ⟩ :: Δ ++ Γ) ✓)
+    cases (Context.perm (by aesop) ok : (⟨x, σ⟩ :: Δ ++ Γ) ✓)
     case cons ok_weak _ =>
     observe perm : (Γ ++ Δ).Perm (Δ ++ Γ)
     by_cases h : x = x' <;> simp only [h]
@@ -134,7 +134,7 @@ lemma subst_strengthened :
         match mem with | _ => aesop
       rw [eq']
       refine Typing.perm perm (weakening der ?_)
-      exact Ctx.perm (id (List.Perm.symm perm)) ok_weak
+      exact Context.perm (id (List.Perm.symm perm)) ok_weak
   case abs σ Γ' t T2 xs ih' ih =>
     apply Typing.abs (xs ∪ {x} ∪ (Δ ++ Γ).dom)
     intros x _
diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
index 9826e5d8..7a24ea23 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
@@ -23,21 +23,21 @@ variable {Var : Type u} {Ty : Type v} [DecidableEq Var]
 namespace LambdaCalculus.LocallyNameless.Stlc
 
 /-- A typing context is a list of free variables and corresponding types. -/
-abbrev Ctx (Var : Type u) (Ty : Type v) := List ((_ : Var) × Ty)
+abbrev Context (Var : Type u) (Ty : Type v) := List ((_ : Var) × Ty)
 
-namespace Ctx
+namespace Context
 
 /-- The domain of a context is the finite set of free variables it uses. -/
 @[simp]
-def dom : Ctx Var Ty → Finset Var := List.toFinset ∘ List.keys
+def dom : Context Var Ty → Finset Var := List.toFinset ∘ List.keys
 
 /-- A well-formed context. -/
-abbrev Ok : Ctx Var Ty → Prop := List.NodupKeys
+abbrev Ok : Context Var Ty → Prop := List.NodupKeys
 
-instance : HasWellFormed (Ctx Var Ty) :=
+instance : HasWellFormed (Context Var Ty) :=
   ⟨Ok⟩
 
-variable {Γ Δ : Ctx Var Ty}
+variable {Γ Δ : Context Var Ty}
 
 /-- Context membership is preserved on permuting a context. -/
 theorem dom_perm_mem_iff (h : Γ.Perm Δ) {x : Var} : 
diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
index e38ff4ef..9aae6ade 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
@@ -49,7 +49,7 @@ theorem preservation_confluence {τ : Ty Base} :
   have ⟨d, bd, cd⟩ := con ab ac
   exact ⟨d, bd, cd, preservation_redex p der (ab.trans bd)⟩
  
-variable [HasFresh Var] [DecidableEq Var] {Γ : Ctx Var (Ty Base)}
+variable [HasFresh Var] [DecidableEq Var] {Γ : Context Var (Ty Base)}
 
 namespace Term.FullBeta
 
@@ -65,7 +65,7 @@ theorem preservation : Γ ⊢ t ∶ τ → (t ⭢βᶠt') → Γ ⊢ t' ∶ τ :
 
 omit [HasFresh Var] [DecidableEq Var] in
 /-- A typed term either full beta reduces or is a value. -/
-theorem progress : ([] : Ctx Var (Ty Base)) ⊢ t ∶ τ → t.Value ∨ ∃ t', t ⭢βᶠ t' := by
+theorem progress : ([] : Context Var (Ty Base)) ⊢ t ∶ τ → t.Value ∨ ∃ t', t ⭢βᶠ t' := by
   intros der
   generalize eq : [] = Γ at der
   induction der

From 15268cbcf1ee9859025277cef5c4a6e81ab31c93 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Wed, 30 Jul 2025 10:58:32 -0400
Subject: [PATCH 26/33] =?UTF-8?q?no=20space=20before=20=E2=9C=93?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 .../LambdaCalculus/LocallyNameless/Stlc/Basic.lean        | 8 ++++----
 .../LambdaCalculus/LocallyNameless/Stlc/Context.lean      | 4 ++--
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
index 2a0534ab..409ba66b 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
@@ -40,7 +40,7 @@ open Term Ty
 @[aesop unsafe [constructors (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]]
 inductive Typing : Context Var (Ty Base) → Term Var → Ty Base → Prop
 /-- Free variables, from a context judgement. -/
-| var : Γ ✓ → ⟨x,σ⟩ ∈ Γ → Typing Γ (fvar x) σ
+| var : Γ✓ → ⟨x,σ⟩ ∈ Γ → Typing Γ (fvar x) σ
 /-- Lambda abstraction. -/
 | abs (L : Finset Var) : (∀ x ∉ L, Typing (⟨x,σ⟩ :: Γ) (t ^ fvar x) τ) → Typing Γ t.abs (σ ⤳ τ) 
 /-- Function application. -/
@@ -69,7 +69,7 @@ theorem perm : Γ.Perm Δ → Γ ⊢ t ∶ τ → Δ ⊢ t ∶ τ := by
 
 /-- Weakening of a typing derivation with an appended context. -/
 lemma weakening_strengthened : 
-    Γ ++ Δ ⊢ t ∶ τ → (Γ ++ Φ ++ Δ) ✓ → (Γ ++ Φ ++ Δ) ⊢ t ∶ τ := by
+    Γ ++ Δ ⊢ t ∶ τ → (Γ ++ Φ ++ Δ)✓ → (Γ ++ Φ ++ Δ) ⊢ t ∶ τ := by
   generalize eq : Γ ++ Δ = Γ_Δ
   intros h
   revert Γ Δ Φ
@@ -85,7 +85,7 @@ lemma weakening_strengthened :
     aesop
 
 /-- Weakening of a typing derivation by an additional context. -/
-lemma weakening : Γ ⊢ t ∶ τ → (Γ ++ Δ) ✓ → Γ ++ Δ ⊢ t ∶ τ := by
+lemma weakening : Γ ⊢ t ∶ τ → (Γ ++ Δ)✓ → Γ ++ Δ ⊢ t ∶ τ := by
   intros der ok
   rw [←List.append_nil (Γ ++ Δ)] at *
   exact weakening_strengthened (by simp_all) ok
@@ -116,7 +116,7 @@ lemma subst_strengthened :
     simp only [subst_fvar]
     rw [←eq] at mem
     rw [←eq] at ok
-    cases (Context.perm (by aesop) ok : (⟨x, σ⟩ :: Δ ++ Γ) ✓)
+    cases (Context.perm (by aesop) ok : (⟨x, σ⟩ :: Δ ++ Γ)✓)
     case cons ok_weak _ =>
     observe perm : (Γ ++ Δ).Perm (Δ ++ Γ)
     by_cases h : x = x' <;> simp only [h]
diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
index 7a24ea23..dc205024 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
@@ -47,11 +47,11 @@ theorem dom_perm_mem_iff (h : Γ.Perm Δ) {x : Var} :
 omit [DecidableEq Var] in
 /-- Context well-formedness is preserved on permuting a context. -/
 @[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
-theorem perm (h : Γ.Perm Δ) : Γ ✓ → Δ ✓ := (List.perm_nodupKeys h).mp
+theorem perm (h : Γ.Perm Δ) : Γ✓ → Δ✓ := (List.perm_nodupKeys h).mp
 
 omit [DecidableEq Var] in
 @[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
-theorem strengthen : (Δ ++ ⟨x, σ⟩ :: Γ) ✓ → (Δ ++ Γ) ✓ := by
+theorem strengthen : (Δ ++ ⟨x, σ⟩ :: Γ)✓ → (Δ ++ Γ)✓ := by
   intros ok
   have sl : List.Sublist (Δ ++ Γ) (Δ ++ ⟨x, σ⟩ :: Γ) := by simp
   exact List.NodupKeys.sublist sl ok

From 189ffbbfab925e76c13888a3c3db6ea056162414 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Wed, 30 Jul 2025 10:59:57 -0400
Subject: [PATCH 27/33] link/reference formatting

---
 .../LambdaCalculus/LocallyNameless/Stlc/Basic.lean            | 4 ++--
 .../LambdaCalculus/LocallyNameless/Stlc/Safety.lean           | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
index 409ba66b..0b9f4e47 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
@@ -13,8 +13,8 @@ The simply typed λ-calculus, with a locally nameless representation of syntax.
 
 ## References
 
-* [A. Chargueraud, *The Locally Nameless Representation*] [Chargueraud2012]
-* See also https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/, from which
+* [A. Chargueraud, *The Locally Nameless Representation*][Chargueraud2012]
+* See also <https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/>, from which
   this is partially adapted
 
 -/
diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
index 9aae6ade..113513f6 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
@@ -16,8 +16,8 @@ Theorems in this file are namespaced by their respective reductions.
 
 ## References
 
-* [A. Chargueraud, *The Locally Nameless Representation*] [Chargueraud2012]
-* See also https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/, from which
+* [A. Chargueraud, *The Locally Nameless Representation*][Chargueraud2012]
+* See also <https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/>, from which
   this is partially adapted
 
 -/

From 5f1a434871595e3bc915fcc672768b75fd53214d Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Wed, 30 Jul 2025 11:02:10 -0400
Subject: [PATCH 28/33] indent inductives

---
 .../LocallyNameless/Stlc/Basic.lean           | 20 +++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
index 0b9f4e47..0e0e161a 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
@@ -27,10 +27,10 @@ namespace LambdaCalculus.LocallyNameless.Stlc
 
 /-- Types of the simply typed lambda calculus. -/
 inductive Ty (Base : Type v)
-/-- A base type, from a typing context. -/
-| base : Base → Ty Base
-/-- A function type. -/
-| arrow : Ty Base → Ty Base → Ty Base
+  /-- A base type, from a typing context. -/
+  | base : Base → Ty Base
+  /-- A function type. -/
+  | arrow : Ty Base → Ty Base → Ty Base
 
 scoped infixr:70 " ⤳ " => Ty.arrow
 
@@ -39,12 +39,12 @@ open Term Ty
 /-- An extrinsic typing derivation for locally nameless terms. -/
 @[aesop unsafe [constructors (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]]
 inductive Typing : Context Var (Ty Base) → Term Var → Ty Base → Prop
-/-- Free variables, from a context judgement. -/
-| var : Γ✓ → ⟨x,σ⟩ ∈ Γ → Typing Γ (fvar x) σ
-/-- Lambda abstraction. -/
-| abs (L : Finset Var) : (∀ x ∉ L, Typing (⟨x,σ⟩ :: Γ) (t ^ fvar x) τ) → Typing Γ t.abs (σ ⤳ τ) 
-/-- Function application. -/
-| app : Typing Γ t (σ ⤳ τ) → Typing Γ t' σ → Typing Γ (app t t') τ
+  /-- Free variables, from a context judgement. -/
+  | var : Γ✓ → ⟨x,σ⟩ ∈ Γ → Typing Γ (fvar x) σ
+  /-- Lambda abstraction. -/
+  | abs (L : Finset Var) : (∀ x ∉ L, Typing (⟨x,σ⟩ :: Γ) (t ^ fvar x) τ) → Typing Γ t.abs (σ ⤳ τ) 
+  /-- Function application. -/
+  | app : Typing Γ t (σ ⤳ τ) → Typing Γ t' σ → Typing Γ (app t t') τ
 
 scoped notation:50 Γ " ⊢ " t " ∶" τ:arg => Typing Γ t τ
 

From c2d348b08b288f9ae182e87b978f7ce5611bd555 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Wed, 30 Jul 2025 11:11:43 -0400
Subject: [PATCH 29/33] Context name convention

---
 .../LambdaCalculus/LocallyNameless/Stlc/Basic.lean | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
index 0e0e161a..6adaab83 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
@@ -50,7 +50,7 @@ scoped notation:50 Γ " ⊢ " t " ∶" τ:arg => Typing Γ t τ
 
 namespace Typing
 
-variable {Γ Δ Φ : Context Var (Ty Base)}
+variable {Γ Δ Θ : Context Var (Ty Base)}
 
 omit [DecidableEq Var] in
 /-- Typing is preserved on permuting a context. -/
@@ -69,18 +69,18 @@ theorem perm : Γ.Perm Δ → Γ ⊢ t ∶ τ → Δ ⊢ t ∶ τ := by
 
 /-- Weakening of a typing derivation with an appended context. -/
 lemma weakening_strengthened : 
-    Γ ++ Δ ⊢ t ∶ τ → (Γ ++ Φ ++ Δ)✓ → (Γ ++ Φ ++ Δ) ⊢ t ∶ τ := by
+    Γ ++ Δ ⊢ t ∶ τ → (Γ ++ Θ ++ Δ)✓ → (Γ ++ Θ ++ Δ) ⊢ t ∶ τ := by
   generalize eq : Γ ++ Δ = Γ_Δ
   intros h
-  revert Γ Δ Φ
-  induction h <;> intros Γ Δ Φ eq ok_Γ_Φ_Δ
+  revert Γ Δ Θ
+  induction h <;> intros Γ Δ Θ eq ok_Γ_Θ_Δ
   case var => aesop
   case app => aesop
   case abs σ Γ' τ t xs ext ih =>
-    apply Typing.abs (xs ∪ (Γ ++ Φ ++ Δ).dom)
+    apply Typing.abs (xs ∪ (Γ ++ Θ ++ Δ).dom)
     intros x _
     have h : ⟨x, σ⟩ :: Γ ++ Δ = ⟨x, σ⟩ :: Γ' := by aesop
-    refine @ih x (by aesop) _ _ Φ h ?_
+    refine @ih x (by aesop) _ _ Θ h ?_
     simp only [HasWellFormed.wf]
     aesop
 
@@ -107,7 +107,7 @@ lemma subst_strengthened :
     (Δ ++ ⟨x, σ⟩ :: Γ) ⊢ t ∶ τ →
     Γ ⊢ s ∶ σ → 
     (Δ ++ Γ) ⊢ (t [x := s]) ∶ τ := by
-  generalize  eq : Δ ++ ⟨x, σ⟩ :: Γ = Φ
+  generalize  eq : Δ ++ ⟨x, σ⟩ :: Γ = Θ
   intros h
   revert Γ Δ
   induction h <;> intros Γ Δ eq der

From a72353b1f8ebe34ba98a9050e9bc2db06bc6d019 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Wed, 30 Jul 2025 11:15:20 -0400
Subject: [PATCH 30/33] naming conventions

---
 .../LambdaCalculus/LocallyNameless/Stlc/Basic.lean   | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
index 6adaab83..db247fb0 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
@@ -68,7 +68,7 @@ theorem perm : Γ.Perm Δ → Γ ⊢ t ∶ τ → Δ ⊢ t ∶ τ := by
     exact ih x mem (by aesop)
 
 /-- Weakening of a typing derivation with an appended context. -/
-lemma weakening_strengthened : 
+lemma weakening_aux : 
     Γ ++ Δ ⊢ t ∶ τ → (Γ ++ Θ ++ Δ)✓ → (Γ ++ Θ ++ Δ) ⊢ t ∶ τ := by
   generalize eq : Γ ++ Δ = Γ_Δ
   intros h
@@ -88,7 +88,7 @@ lemma weakening_strengthened :
 lemma weakening : Γ ⊢ t ∶ τ → (Γ ++ Δ)✓ → Γ ++ Δ ⊢ t ∶ τ := by
   intros der ok
   rw [←List.append_nil (Γ ++ Δ)] at *
-  exact weakening_strengthened (by simp_all) ok
+  exact weakening_aux (by simp_all) ok
 
 omit [DecidableEq Var] in
 /-- Typing derivations exist only for locally closed terms. -/
@@ -103,7 +103,7 @@ variable [HasFresh Var]
 open Term
 
 /-- Substitution for a context weakened by a single type between appended contexts. -/
-lemma subst_strengthened :
+lemma subst_aux :
     (Δ ++ ⟨x, σ⟩ :: Γ) ⊢ t ∶ τ →
     Γ ⊢ s ∶ σ → 
     (Δ ++ Γ) ⊢ (t [x := s]) ∶ τ := by
@@ -147,11 +147,11 @@ lemma subst_strengthened :
     all_goals aesop  
 
 /-- Substitution for a context weakened by a single type. -/
-lemma typing_subst : 
+lemma typing_subst_head : 
     ⟨x, σ⟩ :: Γ ⊢ t ∶ τ  → Γ ⊢ s ∶ σ → Γ ⊢ (t [x := s]) ∶ τ := by
   intros weak der
   rw [←List.nil_append Γ]
-  exact subst_strengthened weak der
+  exact subst_aux weak der
 
 /-- Typing preservation for opening. -/
 @[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
@@ -162,4 +162,4 @@ theorem preservation_opening {xs : Finset Var} :
   intros mem der
   have ⟨fresh, free⟩ := fresh_exists (xs ∪ m.fv)
   rw [subst_intro fresh n m (by aesop) der.lc]
-  exact typing_subst (mem fresh (by aesop)) der
+  exact typing_subst_head (mem fresh (by aesop)) der

From cf2b750a216153acc46d087bdf1b4d4e74d67ebf Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Wed, 30 Jul 2025 11:27:08 -0400
Subject: [PATCH 31/33] style

---
 .../LambdaCalculus/LocallyNameless/Stlc/Basic.lean         | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
index db247fb0..50f36984 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
@@ -54,10 +54,9 @@ variable {Γ Δ Θ : Context Var (Ty Base)}
 
 omit [DecidableEq Var] in
 /-- Typing is preserved on permuting a context. -/
-theorem perm : Γ.Perm Δ → Γ ⊢ t ∶ τ → Δ ⊢ t ∶ τ := by 
-  intros _ der
+theorem perm (ht : Γ ⊢ t ∶τ) (hperm : Γ.Perm Δ) : Δ ⊢ t ∶ τ := by 
   revert Δ
-  induction der <;> intros Δ p
+  induction ht <;> intros Δ p
   case app => aesop
   case var => 
     have := @p.mem_iff
@@ -133,7 +132,7 @@ lemma subst_aux :
         simp only [List.mem_append, List.mem_cons, Sigma.mk.injEq, heq_eq_eq] at mem
         match mem with | _ => aesop
       rw [eq']
-      refine Typing.perm perm (weakening der ?_)
+      refine (weakening der ?_).perm perm
       exact Context.perm (id (List.Perm.symm perm)) ok_weak
   case abs σ Γ' t T2 xs ih' ih =>
     apply Typing.abs (xs ∪ {x} ∪ (Δ ++ Γ).dom)

From 9f8b61f9f954a103fa8367ac14536cb81fae243d Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Mon, 4 Aug 2025 15:50:00 -0400
Subject: [PATCH 32/33] naming conventions

---
 .../LambdaCalculus/LocallyNameless/Stlc/Basic.lean | 14 +++++++-------
 .../LocallyNameless/Stlc/Context.lean              |  4 ++--
 .../LocallyNameless/Stlc/Safety.lean               | 13 +++++++------
 3 files changed, 16 insertions(+), 15 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
index 50f36984..94b8f223 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
@@ -67,7 +67,7 @@ theorem perm (ht : Γ ⊢ t ∶τ) (hperm : Γ.Perm Δ) : Δ ⊢ t ∶ τ := by
     exact ih x mem (by aesop)
 
 /-- Weakening of a typing derivation with an appended context. -/
-lemma weakening_aux : 
+lemma weaken_aux : 
     Γ ++ Δ ⊢ t ∶ τ → (Γ ++ Θ ++ Δ)✓ → (Γ ++ Θ ++ Δ) ⊢ t ∶ τ := by
   generalize eq : Γ ++ Δ = Γ_Δ
   intros h
@@ -84,10 +84,10 @@ lemma weakening_aux :
     aesop
 
 /-- Weakening of a typing derivation by an additional context. -/
-lemma weakening : Γ ⊢ t ∶ τ → (Γ ++ Δ)✓ → Γ ++ Δ ⊢ t ∶ τ := by
+lemma weaken : Γ ⊢ t ∶ τ → (Γ ++ Δ)✓ → Γ ++ Δ ⊢ t ∶ τ := by
   intros der ok
   rw [←List.append_nil (Γ ++ Δ)] at *
-  exact weakening_aux (by simp_all) ok
+  exact weaken_aux (by simp_all) ok
 
 omit [DecidableEq Var] in
 /-- Typing derivations exist only for locally closed terms. -/
@@ -115,7 +115,7 @@ lemma subst_aux :
     simp only [subst_fvar]
     rw [←eq] at mem
     rw [←eq] at ok
-    cases (Context.perm (by aesop) ok : (⟨x, σ⟩ :: Δ ++ Γ)✓)
+    cases (Context.wf_perm (by aesop) ok : (⟨x, σ⟩ :: Δ ++ Γ)✓)
     case cons ok_weak _ =>
     observe perm : (Γ ++ Δ).Perm (Δ ++ Γ)
     by_cases h : x = x' <;> simp only [h]
@@ -132,8 +132,8 @@ lemma subst_aux :
         simp only [List.mem_append, List.mem_cons, Sigma.mk.injEq, heq_eq_eq] at mem
         match mem with | _ => aesop
       rw [eq']
-      refine (weakening der ?_).perm perm
-      exact Context.perm (id (List.Perm.symm perm)) ok_weak
+      refine (weaken der ?_).perm perm
+      exact Context.wf_perm (id (List.Perm.symm perm)) ok_weak
   case abs σ Γ' t T2 xs ih' ih =>
     apply Typing.abs (xs ∪ {x} ∪ (Δ ++ Γ).dom)
     intros x _
@@ -154,7 +154,7 @@ lemma typing_subst_head :
 
 /-- Typing preservation for opening. -/
 @[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
-theorem preservation_opening {xs : Finset Var} :
+theorem preservation_open {xs : Finset Var} :
   (∀ x ∉ xs, ⟨x, σ⟩ :: Γ ⊢ m ^ fvar x ∶ τ) → 
   Γ ⊢ n ∶ σ → Γ ⊢ m ^ n ∶ τ
   := by
diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
index dc205024..0ce7da16 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Context.lean
@@ -47,11 +47,11 @@ theorem dom_perm_mem_iff (h : Γ.Perm Δ) {x : Var} :
 omit [DecidableEq Var] in
 /-- Context well-formedness is preserved on permuting a context. -/
 @[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
-theorem perm (h : Γ.Perm Δ) : Γ✓ → Δ✓ := (List.perm_nodupKeys h).mp
+theorem wf_perm (h : Γ.Perm Δ) : Γ✓ → Δ✓ := (List.perm_nodupKeys h).mp
 
 omit [DecidableEq Var] in
 @[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
-theorem strengthen : (Δ ++ ⟨x, σ⟩ :: Γ)✓ → (Δ ++ Γ)✓ := by
+theorem wf_strengthen : (Δ ++ ⟨x, σ⟩ :: Γ)✓ → (Δ ++ Γ)✓ := by
   intros ok
   have sl : List.Sublist (Δ ++ Γ) (Δ ++ ⟨x, σ⟩ :: Γ) := by simp
   exact List.NodupKeys.sublist sl ok
diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
index 113513f6..ba8ea77a 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
@@ -30,24 +30,25 @@ open Stlc Typing
 
 variable {Var : Type u} {Base : Type v} {R : Term Var → Term Var → Prop}
 
-def preserves (R : Term Var → Term Var → Prop) (Base : Type v) := 
+def PreservesTyping (R : Term Var → Term Var → Prop) (Base : Type v) := 
   ∀ {Γ t t'} {τ : Ty Base}, Γ ⊢ t ∶ τ → R t t' → Γ ⊢ t' ∶ τ
 
 /-- If a reduction preserves types, so does its reflexive transitive closure. -/
 @[aesop safe forward (rule_sets := [LambdaCalculus.LocallyNameless.ruleSet])]
-theorem preservation_redex : preserves R Base → preserves (Relation.ReflTransGen R) Base := by
+theorem redex_preservesTyping : 
+    PreservesTyping R Base → PreservesTyping (Relation.ReflTransGen R) Base := by
   intros _ _ _ _ _ _ redex
   induction redex <;> aesop
 
 open Relation in
 /-- Confluence preserves type preservation. -/
-theorem preservation_confluence {τ : Ty Base} : 
-    Confluence R → preserves R Base → Γ ⊢ a ∶ τ → 
+theorem confluence_preservesTyping {τ : Ty Base} : 
+    Confluence R → PreservesTyping R Base → Γ ⊢ a ∶ τ → 
     (ReflTransGen R) a b → (ReflTransGen R) a c →
     ∃ d, (ReflTransGen R) b d ∧ (ReflTransGen R) c d ∧ Γ ⊢ d ∶ τ := by
   intros con p der ab ac
   have ⟨d, bd, cd⟩ := con ab ac
-  exact ⟨d, bd, cd, preservation_redex p der (ab.trans bd)⟩
+  exact ⟨d, bd, cd, redex_preservesTyping p der (ab.trans bd)⟩
  
 variable [HasFresh Var] [DecidableEq Var] {Γ : Context Var (Ty Base)}
 
@@ -89,4 +90,4 @@ theorem progress : ([] : Context Var (Ty Base)) ⊢ t ∶ τ → t.Value ∨ ∃
       obtain ⟨M', stepM⟩ := step
       exact ⟨M'.app N, FullBeta.appR der_r.lc stepM⟩ 
 
-end Term.FullBeta
+end LambdaCalculus.LocallyNameless.Term.FullBeta

From 37a267d072aed24d49e5d1a0c83d228735d7460d Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Mon, 4 Aug 2025 15:53:18 -0400
Subject: [PATCH 33/33] style

---
 .../LambdaCalculus/LocallyNameless/Stlc/Safety.lean        | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
index ba8ea77a..33c8add3 100644
--- a/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
+++ b/Cslib/Computability/LambdaCalculus/LocallyNameless/Stlc/Safety.lean
@@ -66,10 +66,9 @@ theorem preservation : Γ ⊢ t ∶ τ → (t ⭢βᶠt') → Γ ⊢ t' ∶ τ :
 
 omit [HasFresh Var] [DecidableEq Var] in
 /-- A typed term either full beta reduces or is a value. -/
-theorem progress : ([] : Context Var (Ty Base)) ⊢ t ∶ τ → t.Value ∨ ∃ t', t ⭢βᶠ t' := by
-  intros der
-  generalize eq : [] = Γ at der
-  induction der
+theorem progress {t : Term Var} {τ : Ty Base} (ht : [] ⊢ t ∶τ) : t.Value ∨ ∃ t', t ⭢βᶠ t' := by
+  generalize eq : [] = Γ at ht
+  induction ht
   case var => aesop
   case abs xs mem ih =>
     left