diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean
index c1c20a96..b5f11ca2 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Context.lean
@@ -17,43 +17,96 @@ Contexts as pairs of free variables and types.
 
 universe u v
 
-variable {Var : Type u} {Ty : Type v} [DecidableEq Var]
+variable {α : Type u} {β : Type v}
+
+-- TODO: These are pieces of API that cannot be directly automated by adding `grind` attributes to
+-- `Mathlib.Data.List.Sigma`. We should consider upstreaming them to Mathlib.
+namespace List
+
+variable {β : α → Type v} {l₁ l₂ : List (Sigma β)}
+
+/-- Keys distribute with appending. -/
+theorem keys_append : (l₁ ++ l₂).keys = l₁.keys ++ l₂.keys := by
+  simp [keys]
+
+variable [DecidableEq α] in
+/-- Sublists without duplicate keys preserve lookups. -/
+theorem sublist_dlookup (nd₂ : l₂.NodupKeys) (s : l₁ <+ l₂) (mem : b ∈ l₁.dlookup a) : 
+    b ∈ l₂.dlookup a := by
+  grind [Option.mem_def, → perm_nodupKeys, dlookup_append, => perm_dlookup,
+    → Sublist.exists_perm_append]
+
+@[grind =]
+lemma nodupKeys_middle : (l₁ ++ s :: l₂).NodupKeys ↔ (s :: (l₁ ++ l₂)).NodupKeys := by
+  simp_all [NodupKeys, keys, nodup_middle]
+
+end List
 
 namespace LambdaCalculus.LocallyNameless
 
+variable [DecidableEq α]
+
 /-- A typing context is a list of free variables and corresponding types. -/
-abbrev Context (Var : Type u) (Ty : Type v) := List ((_ : Var) × Ty)
+abbrev Context (α : Type u) (β : Type v) := List ((_ : α) × β)
 
 namespace Context
 
 open List
 
-/-- The domain of a context is the finite set of free variables it uses. -/
-@[simp, grind =]
-def dom : Context Var Ty → Finset Var := toFinset ∘ keys
+-- we would like grind to see through certain notations
+attribute [scoped grind =] Option.mem_def
+attribute [scoped grind _=_] List.append_eq
+attribute [scoped grind =] List.Nodup
+attribute [scoped grind =] List.NodupKeys
+attribute [scoped grind _=_] List.singleton_append
 
-/-- A well-formed context. -/
-abbrev Ok : Context Var Ty → Prop := NodupKeys
+-- a few grinds on Option:
+attribute [scoped grind =] Option.or_eq_some_iff
+attribute [scoped grind =] Option.or_eq_none_iff
 
-instance : HasWellFormed (Context Var Ty) :=
-  ⟨Ok⟩
+-- we would like grind to treat list and finset membership the same
+attribute [scoped grind _=_] List.mem_toFinset
 
-variable {Γ Δ : Context Var Ty}
+-- otherwise, we mostly reuse existing API in `Mathlib.Data.List.Sigma`
+attribute [scoped grind =] List.keys_cons
+attribute [scoped grind =] List.dlookup_cons_eq
+attribute [scoped grind =] List.dlookup_cons_ne
+attribute [scoped grind =] List.dlookup_nil
+attribute [scoped grind _=_] List.dlookup_isSome
+attribute [scoped grind →] List.perm_nodupKeys
 
-/-- Context membership is preserved on permuting a context. -/
-theorem dom_perm_mem_iff (h : Γ.Perm Δ) {x : Var} : x ∈ Γ.dom ↔ x ∈ Δ.dom := by
-  induction h <;> simp_all only [dom, Function.comp_apply, mem_toFinset, keys_cons, mem_cons] 
-  grind
+/-- The domain of a context is the finite set of free variables it uses. -/
+@[simp, grind =]
+def dom (Γ : Context α β) : Finset α := Γ.keys.toFinset
 
-omit [DecidableEq Var] in
-/-- Context well-formedness is preserved on permuting a context. -/
-@[scoped grind →]
-theorem wf_perm (h : Γ.Perm Δ) : Γ✓ → Δ✓ := (List.perm_nodupKeys h).mp
+instance : HasWellFormed (Context α β) :=
+  ⟨NodupKeys⟩
+
+omit [DecidableEq α] in
+@[scoped grind _=_]
+theorem haswellformed_def (Γ : Context α β) : Γ✓ = Γ.NodupKeys := by rfl
+
+variable {Γ Δ : Context α β}
 
-omit [DecidableEq Var] in
+omit [DecidableEq α] in
 /-- Context well-formedness is preserved on removing an element. -/
 @[scoped grind →]
 theorem wf_strengthen (ok : (Δ ++ ⟨x, σ⟩ :: Γ)✓) : (Δ ++ Γ)✓ := by
-  exact List.NodupKeys.sublist (by simp) ok
+  grind [keys_append]
+
+/-- A mapping of values within a context. -/
+@[simp, scoped grind]
+def map_val (f : β → β) (Γ : Context α β) : Context α β := 
+  Γ.map (fun ⟨var,ty⟩ => ⟨var,f ty⟩)
+
+omit [DecidableEq α] in
+/-- A mapping of values preserves keys. -/
+@[scoped grind]
+lemma map_val_keys (f) : Γ.keys = (Γ.map_val f).keys := by
+  induction Γ <;> grind
+
+/-- A mapping of values maps lookups. -/
+lemma map_val_mem (mem : σ ∈ Γ.dlookup x) (f) : f σ ∈ (Γ.map_val f).dlookup x := by
+  induction Γ <;> grind
 
 end LambdaCalculus.LocallyNameless.Context
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean
new file mode 100644
index 00000000..ce0770cb
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Basic.lean
@@ -0,0 +1,107 @@
+/-
+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.Foundations.Data.HasFresh
+import Cslib.Foundations.Syntax.HasSubstitution
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Context
+
+/-! # λ-calculus
+
+The λ-calculus with polymorphism and subtyping, 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 adapted
+
+-/
+
+variable {Var : Type*} [HasFresh Var] [DecidableEq Var]
+
+namespace LambdaCalculus.LocallyNameless.Fsub
+
+/-- Types of the polymorphic lambda calculus. -/
+inductive Ty (Var : Type*)
+  /-- The type ⊤, with a single inhabitant. -/
+  | top : Ty Var
+  /-- Bound variables that appear in a type, using a de-Bruijn index. -/
+  | bvar : ℕ → Ty Var
+  /-- Free type variables. -/
+  | fvar : Var → Ty Var
+  /-- A function type. -/
+  | arrow : Ty Var → Ty Var → Ty Var
+  /-- A universal quantification. -/
+  | all : Ty Var → Ty Var → Ty Var
+  /-- A sum type. -/
+  | sum : Ty Var → Ty Var → Ty Var
+  deriving Inhabited
+
+/-- Syntax of locally nameless lambda terms, with free variables over `Var`. -/
+inductive Term (Var : Type*)
+  /-- Bound term variables that appear under a lambda abstraction, using a de-Bruijn index. -/
+  | bvar : ℕ → Term Var
+  /-- Free term variables. -/
+  | fvar : Var → Term Var
+  /-- Lambda abstraction, introducing a new bound term variable. -/
+  | abs : Ty Var → Term Var → Term Var
+  /-- Function application. -/
+  | app : Term Var → Term Var → Term Var
+  /-- Type abstraction, introducing a new bound type variable. -/
+  | tabs : Ty Var → Term Var → Term Var
+  /-- Type application. -/
+  | tapp : Term Var → Ty Var → Term Var
+  /-- Binding of a term. -/
+  | let' : Term Var → Term Var → Term Var
+  /-- Left constructor of a sum. -/
+  | inl : Term Var → Term Var
+  /-- Right constructor of a sum. -/
+  | inr : Term Var → Term Var
+  /-- Case matching on a sum. -/
+  | case : Term Var → Term Var → Term Var → Term Var
+
+/-- A context binding. -/
+inductive Binding (Var : Type*)
+  /-- Subtype binding. -/
+  | sub : Ty Var → Binding Var
+  /-- Type binding. -/
+  | ty : Ty Var → Binding Var
+  deriving Inhabited
+
+/-- Free variables of a type. -/
+@[scoped grind =]
+def Ty.fv : Ty Var → Finset Var
+| top | bvar _ => {}
+| fvar X => {X}
+| arrow σ τ | all σ τ | sum σ τ => σ.fv ∪ τ.fv
+
+/-- Free variables of a binding. -/
+@[scoped grind =]
+def Binding.fv : Binding Var → Finset Var
+| sub σ | ty σ => σ.fv
+
+/-- Free type variables of a term. -/
+@[scoped grind =]
+def Term.fv_ty : Term Var → Finset Var
+| bvar _ | fvar _ => {}
+| abs σ t₁ | tabs σ t₁ | tapp t₁ σ => σ.fv ∪ t₁.fv_ty
+| inl t₁ | inr t₁ => t₁.fv_ty
+| app t₁ t₂ | let' t₁ t₂ => t₁.fv_ty ∪ t₂.fv_ty
+| case t₁ t₂ t₃ => t₁.fv_ty ∪ t₂.fv_ty ∪ t₃.fv_ty
+
+/-- Free term variables of a term. -/
+@[scoped grind =]
+def Term.fv_tm : Term Var → Finset Var
+| bvar _ => {}
+| fvar x => {x}
+| abs _ t₁ | tabs _ t₁ | tapp t₁ _ | inl t₁ | inr t₁ => t₁.fv_tm
+| app t₁ t₂ | let' t₁ t₂ => t₁.fv_tm ∪ t₂.fv_tm
+| case t₁ t₂ t₃ => t₁.fv_tm ∪ t₂.fv_tm ∪ t₃.fv_tm
+
+/-- A context of bindings. -/
+abbrev Env (Var : Type*) := Context Var (Binding Var)
+
+end LambdaCalculus.LocallyNameless.Fsub
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean
new file mode 100644
index 00000000..68bc3b69
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Opening.lean
@@ -0,0 +1,416 @@
+/-
+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.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic
+
+
+/-! # λ-calculus
+
+The λ-calculus with polymorphism and subtyping, with a locally nameless representation of syntax.
+This file defines opening, local closure, and substitution.
+
+## References
+
+* [A. Chargueraud, *The Locally Nameless Representation*][Chargueraud2012]
+* See also <https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/>, from which
+  this is adapted
+
+-/
+
+variable {Var : Type*} [HasFresh Var] [DecidableEq Var]
+
+namespace LambdaCalculus.LocallyNameless.Fsub
+
+namespace Ty
+
+/-- Variable opening (type opening to type) of the ith bound variable. -/
+@[scoped grind =]
+def openRec (X : ℕ) (δ : Ty Var) : Ty Var → Ty Var
+| top => top
+| bvar Y => if X = Y then δ else bvar Y
+| fvar X => fvar X
+| arrow σ τ => arrow (openRec X δ σ) (openRec X δ τ)
+| all σ τ => all (openRec X δ σ) (openRec (X + 1) δ τ)
+| sum σ τ => sum (openRec X δ σ) (openRec X δ τ)
+
+scoped notation:68 γ "⟦" X " ↝ " δ "⟧ᵞ"=> openRec X δ γ
+
+/-- Variable opening (type opening to type) of the closest binding. -/
+@[scoped grind =]
+def open' (γ δ : Ty Var) := openRec 0 δ γ
+
+scoped infixr:80 " ^ᵞ " => open'
+
+/-- Locally closed types. -/
+inductive LC : Ty Var → Prop
+  | top : LC top
+  | var : LC (fvar X)
+  | arrow : LC σ → LC τ → LC (arrow σ τ)
+  | all (L : Finset Var) : LC σ → (∀ X ∉ L, LC (τ ^ᵞ fvar X)) → LC (all σ τ)
+  | sum : LC σ → LC τ → LC (sum σ τ)
+
+attribute [scoped grind] LC.top LC.var LC.arrow LC.sum
+
+/-- Type substitution. -/
+@[scoped grind =]
+def subst (X : Var) (δ : Ty Var) : Ty Var → Ty Var
+| top => top
+| bvar J => bvar J
+| fvar Y => if Y = X then δ else fvar Y
+| arrow σ τ => arrow (subst X δ σ) (subst X δ τ)
+| all σ τ => all (subst X δ σ) (subst X δ τ)
+| sum σ τ => sum (subst X δ σ) (subst X δ τ)
+
+instance : HasSubstitution (Ty Var) Var (Ty Var) where
+  subst γ X δ := Ty.subst X δ γ
+
+variable {σ τ δ γ : Ty Var}
+
+omit [HasFresh Var] [DecidableEq Var] in
+/-- An opening appearing in both sides of an equality of types can be removed. -/
+lemma openRec_neq_eq {σ τ γ : Ty Var} (neq : X ≠ Y) (h : σ⟦Y ↝ τ⟧ᵞ = σ⟦Y ↝ τ⟧ᵞ⟦X ↝ γ⟧ᵞ) : 
+    σ = σ⟦X ↝ γ⟧ᵞ := by induction σ generalizing Y X <;> grind
+
+/-- A locally closed type is unchanged by opening. -/
+lemma openRec_lc {σ τ : Ty Var} (lc : σ.LC) : σ = σ⟦X ↝ τ⟧ᵞ := by
+  induction lc generalizing X <;> (have := fresh_exists <| free_union Var; grind [openRec_neq_eq])
+
+omit [HasFresh Var] in
+@[scoped grind _=_]
+lemma subst_def : Ty.subst (X : Var) (δ : Ty Var) (γ : Ty Var) = γ[X := δ] := by rfl
+
+omit [HasFresh Var] in
+/-- Substitution of a free variable not present in a type leaves it unchanged. -/
+lemma subst_fresh (nmem : X ∉ γ.fv) (δ : Ty Var) : γ = γ[X := δ] := by
+  induction γ <;> grind
+
+/-- Substitution of a locally closed type distributes with opening. -/
+lemma openRec_subst (Y : ℕ) (σ τ : Ty Var) (lc : δ.LC) (X : Var) : 
+    (σ⟦Y ↝ τ⟧ᵞ)[X := δ] = σ[X := δ]⟦Y ↝ τ[X := δ]⟧ᵞ := by
+  induction σ generalizing Y
+  all_goals grind [openRec_lc]
+
+/-- Specialize `Ty.openRec_subst` to the first opening. -/
+lemma open_subst (σ τ : Ty Var) (lc : δ.LC) (X : Var) : (σ ^ᵞ τ)[X := δ] = σ[X := δ] ^ᵞ τ[X := δ]
+  := openRec_subst 0 σ τ lc X
+
+/-- Specialize `Ty.subst_open` to free variables. -/
+lemma open_subst_var (σ : Ty Var) (neq : Y ≠ X) (lc : δ.LC) :
+    (σ ^ᵞ fvar Y)[X := δ] = (σ[X := δ]) ^ᵞ fvar Y := by grind [open_subst]
+
+omit [HasFresh Var] in
+/-- Opening to a type is equivalent to opening to a free variable and substituting. -/
+lemma openRec_subst_intro (Y : ℕ) (δ : Ty Var) (nmem : X ∉ γ.fv) :
+    γ⟦Y ↝ δ⟧ᵞ = (γ⟦Y ↝ fvar X⟧ᵞ)[X := δ] := by
+  induction γ generalizing δ Y <;> grind
+
+omit [HasFresh Var] in
+/-- Specialize `Ty.openRec_subst_intro` to the first opening. -/
+lemma open_subst_intro (δ : Ty Var) (nmem : X ∉ γ.fv) : γ ^ᵞ δ = (γ ^ᵞ fvar X)[X := δ] := 
+  openRec_subst_intro _ _ nmem
+
+lemma subst_lc (σ_lc : σ.LC) (τ_lc : τ.LC) (X : Var) : σ[X := τ].LC := by
+  induction σ_lc
+  case all => apply LC.all (free_union Var) <;> grind [openRec_subst] 
+  all_goals grind [openRec_subst]
+
+omit [HasFresh Var] in
+lemma nmem_fv_openRec (nmem : X ∉ (σ⟦k ↝ γ⟧ᵞ).fv) : X ∉ σ.fv := by
+  induction σ generalizing k <;> grind
+
+omit [HasFresh Var] in
+lemma nmem_fv_open (nmem : X ∉ (σ ^ᵞ γ).fv) : X ∉ σ.fv := 
+  Ty.nmem_fv_openRec (k := 0) nmem
+
+end Ty
+
+namespace Term
+
+open scoped Ty
+
+/-- Variable opening (term opening to type) of the ith bound variable. -/
+@[scoped grind =]
+def openRec_ty (X : ℕ) (δ : Ty Var) : Term Var → Term Var
+| bvar x => bvar x
+| fvar x => fvar x
+| abs σ t₁ => abs (σ⟦X ↝ δ⟧ᵞ) (openRec_ty X δ t₁)
+| app t₁ t₂ => app (openRec_ty X δ t₁) (openRec_ty X δ t₂)
+| tabs σ t₁ => tabs (σ⟦X ↝ δ⟧ᵞ) (openRec_ty (X + 1) δ t₁)
+| tapp t₁ σ => tapp (openRec_ty X δ t₁) (σ⟦X ↝ δ⟧ᵞ)
+| let' t₁ t₂ => let' (openRec_ty X δ t₁) (openRec_ty X δ t₂)
+| inl t₁ => inl (openRec_ty X δ t₁)
+| inr t₂ => inr (openRec_ty X δ t₂)
+| case t₁ t₂ t₃ => case (openRec_ty X δ t₁) (openRec_ty X δ t₂) (openRec_ty X δ t₃)
+
+scoped notation:68 t "⟦" X " ↝ " δ "⟧ᵗᵞ"=> openRec_ty X δ t
+
+/-- Variable opening (term opening to type) of the closest binding. -/
+@[scoped grind =]
+def open_ty (t : Term Var) (δ : Ty Var) := openRec_ty 0 δ t
+
+scoped infixr:80 " ^ᵗᵞ " => open_ty
+
+/-- Variable opening (term opening to term) of the ith bound variable. -/
+@[scoped grind =]
+def openRec_tm (x : ℕ) (s : Term Var) : Term Var → Term Var
+| bvar y => if x = y then s else (bvar y)
+| fvar x => fvar x
+| abs σ t₁ => abs σ (openRec_tm (x + 1) s t₁)
+| app t₁ t₂ => app (openRec_tm x s t₁) (openRec_tm x s t₂)
+| tabs σ t₁ => tabs σ (openRec_tm x s t₁)
+| tapp t₁ σ => tapp (openRec_tm x s t₁) σ
+| let' t₁ t₂ => let' (openRec_tm x s t₁) (openRec_tm (x + 1) s t₂)
+| inl t₁ => inl (openRec_tm x s t₁)
+| inr t₂ => inr (openRec_tm x s t₂)
+| case t₁ t₂ t₃ => case (openRec_tm x s t₁) (openRec_tm (x + 1) s t₂) (openRec_tm (x + 1) s t₃)
+
+scoped notation:68 t "⟦" x " ↝ " s "⟧ᵗᵗ"=> openRec_tm x s t
+
+/-- Variable opening (term opening to term) of the closest binding. -/
+@[scoped grind =]
+def open_tm (t₁ t₂ : Term Var) := openRec_tm 0 t₂ t₁
+
+scoped infixr:80 " ^ᵗᵗ " => open_tm
+
+/-- Locally closed terms. -/
+inductive LC : Term Var → Prop
+  | var : LC (fvar x)
+  | abs (L : Finset Var) : σ.LC → (∀ x ∉ L, LC (t₁ ^ᵗᵗ fvar x)) → LC (abs σ t₁)
+  | app : LC t₁ → LC t₂ → LC (app t₁ t₂)
+  | tabs (L : Finset Var) : σ.LC → (∀ X ∉ L, LC (t₁ ^ᵗᵞ .fvar X)) → LC (tabs σ t₁)
+  | tapp : LC t₁ → σ.LC → LC (tapp t₁ σ)
+  | let' (L : Finset Var) : LC t₁ → (∀ x ∉ L, LC (t₂ ^ᵗᵗ fvar x)) → LC (let' t₁ t₂)
+  | inl : LC t₁ → LC (inl t₁)
+  | inr : LC t₁ → LC (inr t₁)
+  | case (L : Finset Var) :
+      LC t₁ →
+      (∀ x ∉ L, LC (t₂ ^ᵗᵗ fvar x)) →
+      (∀ x ∉ L, LC (t₃ ^ᵗᵗ fvar x)) →
+      LC (case t₁ t₂ t₃)
+
+attribute [scoped grind] LC.var LC.app LC.inl LC.inr LC.tapp
+
+variable {t : Term Var} {δ : Ty Var}
+
+omit [HasFresh Var] [DecidableEq Var] in
+/-- An opening (term to type) appearing in both sides of an equality of terms can be removed. -/
+lemma openRec_ty_neq_eq (neq : X ≠ Y) (eq : t⟦Y ↝ σ⟧ᵗᵞ = t⟦Y ↝ σ⟧ᵗᵞ⟦X ↝ τ⟧ᵗᵞ) : 
+    t = t⟦X ↝ τ⟧ᵗᵞ := by
+  induction t generalizing X Y <;> grind [Ty.openRec_neq_eq]
+
+omit [HasFresh Var] [DecidableEq Var] in
+/-- Elimination of mixed term and type opening. -/
+@[scoped grind]
+lemma openRec_tm_ty_eq (eq : t⟦x ↝ s⟧ᵗᵗ = t⟦x ↝ s⟧ᵗᵗ⟦y ↝ δ⟧ᵗᵞ) : t = t⟦y ↝ δ⟧ᵗᵞ
+  := by induction t generalizing x y <;> grind
+
+/-- A locally closed term is unchanged by type opening. -/
+@[scoped grind]
+lemma openRec_ty_lc {t : Term Var} (lc : t.LC) : t = t⟦X ↝ σ⟧ᵗᵞ := by
+  induction lc generalizing X
+  case let' | case | tabs | abs =>
+    have := fresh_exists <| free_union Var
+    congr <;> grind [Ty.openRec_lc, openRec_ty_neq_eq]
+  all_goals grind [Ty.openRec_lc]
+
+/-- Substitution of a type within a term. -/
+@[scoped grind =]
+def subst_ty (X : Var) (δ : Ty Var) : Term Var → Term Var
+| bvar x => bvar x
+| fvar x => fvar x
+| abs σ t₁ => abs (σ [X := δ]) (subst_ty X δ t₁)
+| app t₁ t₂ => app (subst_ty X δ t₁) (subst_ty X δ t₂)
+| tabs σ t₁ => tabs (σ [X := δ]) (subst_ty X δ t₁)
+| tapp t₁ σ => tapp (subst_ty X δ t₁) (σ[X := δ])
+| let' t₁ t₂ => let' (subst_ty X δ t₁) (subst_ty X δ t₂)
+| inl t₁ => inl (subst_ty X δ t₁)
+| inr t₁ => inr (subst_ty X δ t₁)
+| case t₁ t₂ t₃ => case (subst_ty X δ t₁) (subst_ty X δ t₂) (subst_ty X δ t₃)
+
+instance : HasSubstitution (Term Var) Var (Ty Var) where
+  subst t X δ := Term.subst_ty X δ t
+
+omit [HasFresh Var] in
+@[scoped grind _=_]
+lemma subst_ty_def : subst_ty (X : Var) (δ : Ty Var) (t : Term Var) = t[X := δ] := by rfl
+
+omit [HasFresh Var] in
+/-- Substitution of a free type variable not present in a term leaves it unchanged. -/
+lemma subst_ty_fresh (nmem : X ∉ t.fv_ty) (δ : Ty Var) : t = t [X := δ] := 
+  by induction t <;> grind [Ty.subst_fresh]
+
+/-- Substitution of a locally closed type distributes with term opening to a type . -/
+lemma openRec_ty_subst_ty (Y : ℕ) (t : Term Var) (σ : Ty Var) (lc : δ.LC) (X : Var) : 
+    (t⟦Y ↝ σ⟧ᵗᵞ)[X := δ] = (t[X := δ])⟦Y ↝  σ[X := δ]⟧ᵗᵞ := by
+  induction t generalizing Y <;> grind [Ty.openRec_subst]
+
+/-- Specialize `Term.openRec_ty_subst` to the first opening. -/
+lemma open_ty_subst_ty (t : Term Var) (σ : Ty Var) (lc : δ.LC) (X : Var) :
+     (t ^ᵗᵞ σ)[X := δ] = t[X := δ] ^ᵗᵞ σ[X := δ] := openRec_ty_subst_ty 0 t σ lc X
+
+/-- Specialize `Term.open_ty_subst` to free type variables. -/
+lemma open_ty_subst_ty_var (t : Term Var) (neq : Y ≠ X) (lc : δ.LC) :
+    (t ^ᵗᵞ .fvar Y)[X := δ] = t[X := δ] ^ᵗᵞ .fvar Y := by grind [open_ty_subst_ty]
+
+omit [HasFresh Var]
+
+/-- Opening a term to a type is equivalent to opening to a free variable and substituting. -/
+lemma openRec_ty_subst_ty_intro (Y : ℕ) (t : Term Var) (nmem : X ∉ t.fv_ty) : 
+  t⟦Y ↝ δ⟧ᵗᵞ = (t⟦Y ↝ Ty.fvar X⟧ᵗᵞ)[X := δ] := by
+  induction t generalizing X δ Y <;> grind [Ty.openRec_subst_intro]
+
+/-- Specialize `Term.openRec_ty_subst_ty_intro` to the first opening. -/
+lemma open_ty_subst_ty_intro (t : Term Var) (δ : Ty Var) (nmem : X ∉ t.fv_ty) : 
+    t ^ᵗᵞ δ = (t ^ᵗᵞ Ty.fvar X)[X := δ] := openRec_ty_subst_ty_intro _ _ nmem
+
+/-- Substitution of a term within a term. -/
+@[scoped grind =]
+def subst_tm (x : Var) (s : Term Var) : Term Var → Term Var
+| bvar x => bvar x
+| fvar y => if y = x then s else fvar y
+| abs σ t₁ => abs σ (subst_tm x s t₁)
+| app t₁ t₂ => app (subst_tm x s t₁) (subst_tm x s t₂)
+| tabs σ t₁ => tabs σ (subst_tm x s t₁)
+| tapp t₁ σ => tapp (subst_tm x s t₁) σ
+| let' t₁ t₂ => let' (subst_tm x s t₁) (subst_tm x s t₂)
+| inl t₁ => inl (subst_tm x s t₁)
+| inr t₁ => inr (subst_tm x s t₁)
+| case t₁ t₂ t₃ => case (subst_tm x s t₁) (subst_tm x s t₂) (subst_tm x s t₃)
+
+instance : HasSubstitution (Term Var) Var (Term Var) where
+  subst t x s := Term.subst_tm x s t
+
+@[scoped grind _=_]
+lemma subst_tm_def : subst_tm (x : Var) (s : Term Var) (t : Term Var) = t[x := s] := by rfl
+
+omit [DecidableEq Var] in
+/-- An opening (term to term) appearing in both sides of an equality of terms can be removed. -/
+lemma openRec_tm_neq_eq (neq : x ≠ y) (eq : t⟦y ↝ s₁⟧ᵗᵗ = t⟦y ↝ s₁⟧ᵗᵗ⟦x ↝ s₂⟧ᵗᵗ) : 
+    t = t⟦x ↝ s₂⟧ᵗᵗ := by
+  induction t generalizing x y <;> grind
+
+omit [DecidableEq Var] in
+/-- Elimination of mixed term and type opening. -/
+lemma openRec_ty_tm_eq (eq : t⟦Y ↝ σ⟧ᵗᵞ = t⟦Y ↝ σ⟧ᵗᵞ⟦x ↝ s⟧ᵗᵗ) : t = t⟦x ↝ s⟧ᵗᵗ := by
+  induction t generalizing x Y <;> grind
+
+variable [HasFresh Var]
+
+/-- A locally closed term is unchanged by term opening. -/
+@[scoped grind]
+lemma openRec_tm_lc (lc : t.LC) : t = t⟦x ↝ s⟧ᵗᵗ := by
+  induction lc generalizing x
+  case let' | case | tabs | abs =>
+    have := fresh_exists <| free_union Var
+    congr <;> grind [openRec_tm_neq_eq, openRec_ty_tm_eq]
+  all_goals grind
+
+variable {t s : Term Var} {δ : Ty Var} {x : Var}
+
+omit [HasFresh Var] in
+/-- Substitution of a free term variable not present in a term leaves it unchanged. -/
+lemma subst_tm_fresh (nmem : x ∉ t.fv_tm) (s : Term Var) : t = t[x := s] := by
+  induction t <;> grind
+
+/-- Substitution of a locally closed term distributes with term opening to a term. -/
+lemma openRec_tm_subst_tm (y : ℕ) (t₁ t₂ : Term Var) (lc : s.LC) (x : Var) :
+    (t₁⟦y ↝ t₂⟧ᵗᵗ)[x := s] = (t₁[x := s])⟦y ↝  t₂[x := s]⟧ᵗᵗ := by
+  induction t₁ generalizing y <;> grind
+
+/-- Specialize `Term.openRec_tm_subst_tm` to the first opening. -/
+lemma open_tm_subst_tm (t₁ t₂ : Term Var) (lc : s.LC) (x : Var) :
+    (t₁ ^ᵗᵗ t₂)[x := s] = (t₁[x := s]) ^ᵗᵗ t₂[x := s] := openRec_tm_subst_tm 0 t₁ t₂ lc x
+
+/-- Specialize `Term.openRec_tm_subst_tm` to free term variables. -/ 
+lemma open_tm_subst_tm_var (t : Term Var) (neq : y ≠ x) (lc : s.LC) :
+     (t ^ᵗᵗ fvar y)[x := s] = (t[x := s]) ^ᵗᵗ fvar y := by grind [open_tm_subst_tm]
+
+/-- Substitution of a locally closed type distributes with term opening to a term. -/
+lemma openRec_tm_subst_ty (y : ℕ) (t₁ t₂ : Term Var) (δ : Ty Var) (X : Var) :
+    (t₁⟦y ↝ t₂⟧ᵗᵗ)[X := δ] = (t₁[X := δ])⟦y ↝  t₂[X := δ]⟧ᵗᵗ := by
+  induction t₁ generalizing y <;> grind
+
+/-- Specialize `Term.openRec_tm_subst_ty` to the first opening -/
+lemma open_tm_subst_ty (t₁ t₂ : Term Var) (δ : Ty Var) (X : Var) :
+    (t₁ ^ᵗᵗ t₂)[X := δ] = (t₁[X := δ]) ^ᵗᵗ t₂[X := δ] := openRec_tm_subst_ty 0 t₁ t₂ δ X
+
+/-- Specialize `Term.open_tm_subst_ty` to free term variables -/
+lemma open_tm_subst_ty_var (t₁ : Term Var) (δ : Ty Var) (X y : Var) :
+    (t₁ ^ᵗᵗ fvar y)[X := δ] = (t₁[X := δ]) ^ᵗᵗ fvar y := by grind [open_tm_subst_ty]
+
+/-- Substitution of a locally closed term distributes with term opening to a type. -/
+lemma openRec_ty_subst_tm (Y : ℕ) (t : Term Var) (δ : Ty Var) (lc : s.LC) (x : Var) :
+    (t⟦Y ↝ δ⟧ᵗᵞ)[x := s] = t[x := s]⟦Y ↝ δ⟧ᵗᵞ := by
+  induction t generalizing Y <;> grind
+
+/-- Specialize `Term.openRec_ty_subst_tm` to the first opening. -/
+lemma open_ty_subst_tm (t : Term Var) (δ : Ty Var) (lc : s.LC) (x : Var) :
+    (t ^ᵗᵞ δ)[x := s] = t[x := s] ^ᵗᵞ δ := openRec_ty_subst_tm 0 t δ lc x
+
+/-- Specialize `Term.open_ty_subst_tm` to free type variables. -/
+lemma open_ty_subst_tm_var (t : Term Var) (lc : s.LC) (x Y : Var) :
+    (t ^ᵗᵞ .fvar Y)[x := s] = t[x := s] ^ᵗᵞ .fvar Y := open_ty_subst_tm _ _ lc _
+
+omit [HasFresh Var]
+
+/-- Opening a term to a term is equivalent to opening to a free variable and substituting. -/
+lemma openRec_tm_subst_tm_intro (y : ℕ) (t s : Term Var) (nmem : x ∉ t.fv_tm) :
+    t⟦y ↝ s⟧ᵗᵗ = (t⟦y ↝ fvar x⟧ᵗᵗ)[x := s] := by
+  induction t generalizing y <;> grind
+
+/-- Specialize `Term.openRec_tm_subst_tm_intro` to the first opening. -/
+lemma open_tm_subst_tm_intro (t s : Term Var) (nmem : x ∉ t.fv_tm) :
+    t ^ᵗᵗs = (t ^ᵗᵗ fvar x)[x := s] := openRec_tm_subst_tm_intro _ _ _ nmem
+
+variable [HasFresh Var]
+
+lemma subst_ty_lc (t_lc : t.LC) (δ_lc : δ.LC) (X : Var) : t[X := δ].LC := by
+  induction t_lc
+  case' abs  => apply LC.abs (free_union Var)
+  case' tabs => apply LC.tabs (free_union Var)
+  case' let' => apply LC.let' (free_union Var)
+  case' case => apply LC.case (free_union Var)
+  all_goals grind [Ty.subst_lc, open_tm_subst_ty_var, openRec_ty_subst_ty]
+
+lemma subst_tm_lc (t_lc : t.LC) (s_lc : s.LC) (x : Var) : t[x := s].LC := by
+  induction t_lc
+  case' abs  => apply LC.abs (free_union Var)
+  case' let' => apply LC.let' (free_union Var)
+  case' case => apply LC.case (free_union Var)
+  case' tabs => apply LC.tabs (free_union Var)
+  all_goals grind [open_tm_subst_tm_var, open_ty_subst_tm_var]
+
+end Term
+
+namespace Binding
+
+omit [HasFresh Var]
+
+/-- Binding substitution of types. -/
+@[scoped grind =]
+def subst (X : Var) (δ : Ty Var) : Binding Var → Binding Var
+| sub γ => sub <| γ[X := δ]
+| ty  γ => ty  <| γ[X := δ]
+
+instance : HasSubstitution (Binding Var) Var (Ty Var) where
+  subst γ X δ := Binding.subst X δ γ
+
+variable {δ γ : Ty Var} {X : Var}
+
+@[scoped grind _=_]
+lemma subst_sub : (sub γ)[X := δ] = sub (γ[X := δ]) := by rfl
+
+@[scoped grind _=_]
+lemma subst_ty : (ty γ)[X := δ] = ty (γ[X := δ]) := by rfl
+
+open scoped Ty in
+/-- Substitution of a free variable not present in a binding leaves it unchanged. -/
+lemma subst_fresh {γ : Binding Var} (nmem : X ∉ γ.fv) (δ : Ty Var) : γ = γ[X := δ] := by
+  induction γ <;> grind [Ty.subst_fresh]
+
+end Binding
+
+end LambdaCalculus.LocallyNameless.Fsub
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean
new file mode 100644
index 00000000..87e7a2ec
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Reduction.lean
@@ -0,0 +1,123 @@
+/-
+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.Languages.LambdaCalculus.LocallyNameless.Fsub.Opening
+import Cslib.Foundations.Semantics.ReductionSystem.Basic
+
+/-! # λ-calculus
+
+The λ-calculus with polymorphism and subtyping, with a locally nameless representation of syntax.
+This file defines a call-by-value reduction.
+
+## References
+
+* [A. Chargueraud, *The Locally Nameless Representation*][Chargueraud2012]
+* See also <https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/>, from which
+  this is adapted
+
+-/
+
+variable {Var : Type*}
+
+namespace LambdaCalculus.LocallyNameless.Fsub
+
+namespace Term
+
+/-- Existential predicate for being a locally closed body of an abstraction. -/
+@[scoped grind =]
+def body (t : Term Var) := ∃ L : Finset Var, ∀ x ∉ L, LC (t ^ᵗᵗ fvar x)
+
+section
+
+variable {t₁ t₂ t₃ : Term Var}
+
+variable [DecidableEq Var]
+
+/-- Locally closed let bindings have a locally closed body. -/
+@[scoped grind _=_]
+lemma body_let : (let' t₁ t₂).LC ↔ t₁.LC ∧ t₂.body := by
+  constructor <;> intro h <;> cases h
+  case mp.let' L _ _ =>
+    split_ands
+    · grind
+    · exists L
+  case mpr.intro body =>
+    obtain ⟨_, _⟩ := body
+    apply LC.let' (free_union Var) <;> grind
+
+/-- Locally closed case bindings have a locally closed bodies. -/
+@[scoped grind _=_]
+lemma body_case : (case t₁ t₂ t₃).LC ↔ t₁.LC ∧ t₂.body ∧ t₃.body := by
+  constructor <;> intro h
+  case mp =>
+    cases h with | case L =>
+    split_ands
+    · grind
+    · exists L
+    · exists L
+  case mpr =>
+    obtain ⟨_, ⟨_, _⟩, ⟨_, _⟩⟩ := h
+    apply LC.case (free_union Var) <;> grind
+
+variable [HasFresh Var]
+
+/-- Opening a body preserves local closure. -/
+@[scoped grind <=]
+lemma open_tm_body (body : t₁.body) (lc : t₂.LC) : (t₁ ^ᵗᵗ t₂).LC := by
+  cases body
+  have := fresh_exists <| free_union [fv_tm] Var
+  grind [subst_tm_lc, open_tm_subst_tm_intro]
+
+end
+
+/-- Values are irreducible terms. -/
+@[grind]
+inductive Value : Term Var → Prop
+  | abs : LC (abs σ t₁) → Value (abs σ t₁)
+  | tabs : LC (tabs σ t₁) → Value (tabs σ t₁)
+  | inl : Value t₁ → Value (inl t₁)
+  | inr : Value t₁ → Value (inr t₁)
+
+@[grind →]
+lemma Value.lc {t : Term Var} (val : t.Value) : t.LC := by
+  induction val <;> grind
+
+/-- The call-by-value reduction relation. -/
+@[grind, reduction_sys rs "βᵛ"]
+inductive Red : Term Var → Term Var → Prop
+  | appₗ : LC t₂ → Red t₁ t₁' → Red (app t₁ t₂) (app t₁' t₂)
+  | appᵣ : Value t₁ → Red t₂ t₂' → Red (app t₁ t₂) (app t₁ t₂')
+  | tapp : σ.LC → Red t₁ t₁' → Red (tapp t₁ σ) (tapp t₁' σ)
+  | abs : LC (abs σ t₁) → Value t₂ → Red (app (abs σ t₁) t₂) (t₁ ^ᵗᵗ t₂)
+  | tabs : LC (tabs σ t₁) → τ.LC → Red (tapp (tabs σ t₁) τ) (t₁ ^ᵗᵞ τ)
+  | let_bind : Red t₁ t₁' → t₂.body → Red (let' t₁ t₂) (let' t₁' t₂)
+  | let_body : Value t₁ → t₂.body → Red (let' t₁ t₂) (t₂ ^ᵗᵗ t₁)
+  | inl : Red t₁ t₁' → Red (inl t₁) (inl t₁')
+  | inr : Red t₁ t₁' → Red (inr t₁) (inr t₁')
+  | case : Red t₁ t₁' → t₂.body → t₃.body → Red (case t₁ t₂ t₃) (case t₁' t₂ t₃)
+  | case_inl : Value t₁ → t₂.body → t₃.body → Red (case (inl t₁) t₂ t₃) (t₂ ^ᵗᵗ t₁)
+  | case_inr : Value t₁ → t₂.body → t₃.body → Red (case (inr t₁) t₂ t₃) (t₃ ^ᵗᵗ t₁)
+
+@[grind _=_]
+private lemma rs_eq {t t' : Term Var} : t ⭢βᵛ t' ↔ Red t t' := by
+  have : (@rs Var).Red = Red := by rfl
+  simp_all
+
+variable [HasFresh Var] [DecidableEq Var] in
+/-- Terms of a reduction are locally closed. -/
+lemma Red.lc {t t' : Term Var} (red : t ⭢βᵛ t') : t.LC ∧ t'.LC := by
+  induction red
+  case abs lc _ | tabs lc _ => 
+    split_ands
+    · grind
+    · cases lc
+      have := fresh_exists <| free_union [fv_tm, fv_ty] Var
+      grind [subst_tm_lc, subst_ty_lc, open_tm_subst_tm_intro, open_ty_subst_ty_intro]
+  all_goals grind
+
+end Term
+
+end LambdaCalculus.LocallyNameless.Fsub
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean
new file mode 100644
index 00000000..27153349
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Safety.lean
@@ -0,0 +1,153 @@
+/-
+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.Languages.LambdaCalculus.LocallyNameless.Fsub.Typing
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Reduction
+
+/-! # λ-calculus
+
+The λ-calculus with polymorphism and subtyping, with a locally nameless representation of syntax.
+This file proves type safety.
+
+## References
+
+* [A. Chargueraud, *The Locally Nameless Representation*][Chargueraud2012]
+* See also <https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/>, from which
+  this is adapted
+
+-/
+
+variable {Var : Type*} [HasFresh Var] [DecidableEq Var]
+
+namespace LambdaCalculus.LocallyNameless.Fsub
+
+open Context List Env.Wf Term Ty
+
+variable {t : Term Var}
+
+/-- Any reduction step preserves typing. -/
+lemma Typing.preservation (der : Typing Γ t τ) (step : t ⭢βᵛ t') : Typing Γ t' τ := by
+  induction der generalizing t' 
+  case app Γ _ σ τ _ _ _ _ _ => 
+    cases step
+    case appₗ | appᵣ => grind
+    case abs der _ _ =>
+      have sub : Sub Γ (σ.arrow τ) (σ.arrow τ) := by grind [Sub.refl]
+      have ⟨_, _, ⟨_, _⟩⟩ := der.abs_inv sub
+      have ⟨_, _⟩ := fresh_exists <| free_union [fv_tm] Var
+      grind [open_tm_subst_tm_intro, subst_tm, Sub.weaken]
+  case tapp Γ _ σ τ σ' _ _ _ =>
+    cases step
+    case tabs der _ _ =>
+      have sub : Sub Γ (σ.all τ) (σ.all τ) := by grind [Sub.refl]
+      have ⟨_, _, ⟨_, _⟩⟩ := der.tabs_inv sub
+      have ⟨X, _⟩ := fresh_exists <| free_union [Ty.fv, fv_ty] Var
+      have : Γ = (Context.map_val (·[X:=σ']) []) ++ Γ := by simp
+      rw [open_ty_subst_ty_intro (X := X), open_subst_intro (X := X)] <;> grind [subst_ty]
+    case tapp => grind
+  case let' Γ _ _ _ _ L der _ ih₁ _ => 
+    cases step
+    case let_bind red₁ _ => apply Typing.let' L (ih₁ red₁); grind
+    case let_body =>
+      have ⟨x, _⟩ := fresh_exists <| free_union [fv_tm] Var
+      grind [open_tm_subst_tm_intro, subst_tm]
+  case case Γ _ σ τ _ _ _ L _ _ _ ih₁ _ _ => 
+    have sub : Sub Γ (σ.sum τ) (σ.sum τ) := by grind [Sub.refl]
+    have : Γ = [] ++ Γ := by rfl
+    cases step
+    case «case» red₁ _ _ => apply Typing.case L (ih₁ red₁) <;> grind
+    case case_inl der _ _ => 
+      have ⟨_, ⟨_, _⟩⟩ := der.inl_inv sub
+      have ⟨x, _⟩ := fresh_exists <| free_union [fv_tm] Var
+      grind [open_tm_subst_tm_intro, subst_tm]
+    case case_inr der _ _ => 
+      have ⟨_, ⟨_, _⟩⟩ := der.inr_inv sub
+      have ⟨x, _⟩ := fresh_exists <| free_union [fv_tm] Var
+      grind [open_tm_subst_tm_intro, subst_tm]
+  all_goals grind [cases Red]
+
+/-- Any typable term either has a reduction step or is a value. -/
+lemma Typing.progress (der : Typing [] t τ) : t.Value ∨ ∃ t', t ⭢βᵛ t' := by
+  generalize eq : [] = Γ at der
+  have der' : Typing Γ t τ := by assumption
+  induction der <;> subst eq <;> simp only [forall_const] at *
+  case var mem => grind
+  case app t₁ _ _ t₂ l r ih_l ih_r => 
+    right
+    cases ih_l l with
+    | inl val_l => 
+        cases ih_r r with
+        | inl val_r => 
+            have ⟨σ, t₁, eq⟩ := l.canonical_form_abs val_l
+            exists t₁ ^ᵗᵗ t₂
+            grind
+        | inr red_r => 
+            obtain ⟨t₂', _⟩ := red_r
+            exists t₁.app t₂'
+            grind
+    | inr red_l => 
+        obtain ⟨t₁', _⟩ := red_l
+        exists t₁'.app t₂
+        grind
+  case tapp σ' der _ ih => 
+    right
+    specialize ih der
+    cases ih with
+    | inl val => 
+        obtain ⟨_, t, _⟩ := der.canonical_form_tabs val
+        exists t ^ᵗᵞ σ'
+        grind
+    | inr red => 
+        obtain ⟨t', _⟩ := red
+        exists .tapp t' σ'
+        grind
+  case let' t₁ σ t₂ τ L der _ _ ih => 
+    right
+    cases ih der with
+    | inl _ => 
+        exists t₂ ^ᵗᵗ t₁
+        grind
+    | inr red => 
+        obtain ⟨t₁', _⟩ := red
+        exists t₁'.let' t₂
+        grind
+  case inl der _ ih =>
+    cases (ih der) with
+    | inl val => grind
+    | inr red => 
+        right
+        obtain ⟨t', _⟩ := red
+        exists .inl t'
+        grind
+  case inr der _ ih =>
+    cases (ih der) with
+    | inl val => grind
+    | inr red => 
+        right
+        obtain ⟨t', _⟩ := red
+        exists .inr t'
+        grind
+  case case t₁ _ _ t₂ _ t₃ _ der _ _ _ _ ih => 
+    right
+    cases ih der with
+    | inl val => 
+        have ⟨t₁, lr⟩ := der.canonical_form_sum val
+        cases lr <;> [exists t₂ ^ᵗᵗ t₁; exists t₃ ^ᵗᵗ t₁] <;> grind
+    | inr red => 
+        obtain ⟨t₁', _⟩ := red
+        exists t₁'.case t₂ t₃
+        grind
+  case sub => grind
+  case abs σ _ τ L _ _=> 
+    left
+    constructor
+    apply LC.abs L <;> grind [cases Env.Wf, cases Term.LC]
+  case tabs L _ _=>
+    left
+    constructor
+    apply LC.tabs L <;> grind [cases Env.Wf, cases Term.LC]
+
+end LambdaCalculus.LocallyNameless.Fsub
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean
new file mode 100644
index 00000000..7a11bba5
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean
@@ -0,0 +1,158 @@
+/-
+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.Languages.LambdaCalculus.LocallyNameless.Fsub.WellFormed
+
+/-! # λ-calculus
+
+The λ-calculus with polymorphism and subtyping, with a locally nameless representation of syntax.
+This file defines the subtyping relation.
+
+## References
+
+* [A. Chargueraud, *The Locally Nameless Representation*][Chargueraud2012]
+* See also <https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/>, from which
+  this is adapted
+
+-/
+
+variable {Var : Type*} [DecidableEq Var]
+
+namespace LambdaCalculus.LocallyNameless.Fsub
+
+open Ty
+
+/-- The subtyping relation. -/
+inductive Sub : Env Var → Ty Var → Ty Var → Prop
+  | top : Γ.Wf → σ.Wf Γ → Sub Γ σ top
+  | refl_tvar : Γ.Wf → (fvar X).Wf Γ → Sub Γ (fvar X) (fvar X)
+  | trans_tvar : Binding.sub σ ∈ Γ.dlookup X → Sub Γ σ σ' → Sub Γ (fvar X) σ'
+  | arrow : Sub Γ σ σ' → Sub Γ τ' τ → Sub Γ (arrow σ' τ') (arrow σ τ)
+  | all (L : Finset Var) :
+      Sub Γ σ σ' →
+      (∀ X ∉ L, Sub (⟨X, Binding.sub σ⟩ :: Γ) (τ' ^ᵞ fvar X) (τ ^ᵞ fvar X)) →
+      Sub Γ (all σ' τ') (all σ τ)
+  | sum : Sub Γ σ' σ → Sub Γ τ' τ → Sub Γ (sum σ' τ') (sum σ τ)
+
+namespace Sub
+
+open Context List Ty.Wf Env.Wf Binding
+
+attribute [scoped grind] Sub.top Sub.refl_tvar Sub.trans_tvar Sub.arrow Sub.sum
+
+variable {Γ Δ Θ : Env Var} {σ τ δ : Ty Var}
+
+/-- Subtypes have well-formed contexts and types. -/
+@[grind →]
+lemma wf (Γ : Env Var) (σ σ' : Ty Var) (sub : Sub Γ σ σ') : Γ.Wf ∧ σ.Wf Γ ∧ σ'.Wf Γ := by
+  induction sub with
+  | all => 
+    refine ⟨by grind, ?_, ?_⟩ <;>
+    apply Wf.all (free_union Var) <;> grind [Wf.narrow_cons, cases Env.Wf, cases LC]
+  | _ => grind
+
+/-- Subtypes are reflexive when well-formed. -/
+lemma refl (wf_Γ : Γ.Wf) (wf_σ : σ.Wf Γ) : Sub Γ σ σ := by
+  induction wf_σ with
+  | all => apply all (free_union [Context.dom] Var) <;> grind
+  | _ => grind
+
+/-- Weakening of subtypes. -/
+lemma weaken (sub : Sub (Γ ++ Θ) σ σ') (wf : (Γ ++ Δ ++ Θ).Wf) : Sub (Γ ++ Δ ++ Θ) σ σ' := by
+  generalize eq : Γ ++ Θ = ΓΘ at sub
+  induction sub generalizing Γ 
+  case all => 
+    subst eq
+    apply all (free_union [Context.dom] Var) <;> grind [keys_append]
+  all_goals grind [Ty.Wf.weaken, <= sublist_dlookup]
+
+lemma weaken_head (sub : Sub Δ σ σ') (wf : (Γ ++ Δ).Wf) : Sub (Γ ++ Δ) σ σ' := by
+  have eq : Γ ++ Δ = [] ++ Γ ++ Δ := by grind
+  grind [weaken]
+
+lemma narrow_aux
+    (trans : ∀ Γ σ τ, Sub Γ σ δ → Sub Γ δ τ → Sub Γ σ τ)
+    (sub₁ : Sub (Γ ++ ⟨X, Binding.sub δ⟩ :: Δ) σ τ) (sub₂ : Sub Δ δ' δ) : 
+      Sub (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) σ τ := by
+  generalize eq : Γ ++ ⟨X, Binding.sub δ⟩ :: Δ = Θ at sub₁ 
+  induction sub₁ generalizing Γ δ
+  case trans_tvar σ _ σ' X' mem sub ih => 
+    have p : ∀ δ, Γ ++ ⟨X, Binding.sub δ⟩ :: Δ ~ ⟨X, Binding.sub δ⟩ :: (Γ ++ Δ) := 
+      by grind [perm_middle]
+    have := perm_dlookup (p := p δ')
+    have := perm_dlookup (p := p δ)
+    grind [Sub.weaken, sublist_append_of_sublist_right]
+  case all => apply Sub.all (free_union Var) <;> grind
+  all_goals grind [Env.Wf.narrow, Ty.Wf.narrow]
+
+@[grind →]
+lemma trans : Sub Γ σ δ → Sub Γ δ τ → Sub Γ σ τ := by
+  intro sub₁ sub₂ 
+  have δ_lc : δ.LC := by grind
+  induction δ_lc generalizing Γ σ τ
+  case top => cases sub₁ <;> cases sub₂ <;> grind
+  case var X =>
+    generalize eq : fvar X = γ at sub₁ 
+    induction sub₁ <;> grind [cases Sub]
+  case arrow σ' τ' _ _ _ _ => 
+    generalize eq : σ'.arrow τ' = γ at sub₁
+    induction sub₁ <;> grind [cases Sub]
+  case sum σ' τ' _ _ _ _ => 
+    generalize eq : σ'.sum τ' = γ at sub₁
+    induction sub₁ <;> grind [cases Sub]
+  case all σ' τ' _ _ _ _ _ => 
+    generalize eq : σ'.all τ' = γ at sub₁
+    induction sub₁
+    case all =>
+      cases eq
+      cases sub₂
+      case refl.top Γ σ'' τ'' _ _ _ _ _ _ _ => 
+        have : Sub Γ (σ''.all τ'') (σ'.all τ') := by apply all (free_union Var) <;> grind
+        grind
+      case refl.all Γ _ _ _ _ _ σ _ _ _ _ _ _ => 
+        apply all (free_union Var)
+        · grind
+        · intro X nmem
+          have eq : ∀ σ, ⟨X, Binding.sub σ⟩ :: Γ = [] ++ ⟨X, Binding.sub σ⟩ :: Γ := by grind
+          grind [Sub.narrow_aux]
+    all_goals grind
+
+instance (Γ : Env Var) : Trans (Sub Γ) (Sub Γ) (Sub Γ) := 
+  ⟨Sub.trans⟩
+
+/-- Narrowing of subtypes. -/
+lemma narrow (sub_δ : Sub Δ δ δ') (sub_narrow : Sub (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) σ τ) :
+    Sub (Γ ++ ⟨X, Binding.sub δ⟩ :: Δ) σ τ := by
+  apply narrow_aux (δ := δ') <;> grind
+
+variable [HasFresh Var] in
+/-- Subtyping of substitutions. -/
+lemma map_subst (sub₁ : Sub (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) σ τ) (sub₂ : Sub Δ δ δ') :
+    Sub (Γ.map_val (·[X:=δ]) ++ Δ) (σ[X:=δ]) (τ[X:=δ]) := by
+  generalize eq : Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ = Θ at sub₁
+  induction sub₁ generalizing Γ
+  case all => apply Sub.all (free_union Var) <;> grind [open_subst_var]
+  case trans_tvar σ _ _ X' _ _ _ => 
+    have := map_subst_nmem Δ X δ
+    have : Γ ++ ⟨X, .sub δ'⟩ :: Δ ~ ⟨X, .sub δ'⟩ :: (Γ ++ Δ) := perm_middle
+    have : .sub σ ∈ dlookup X' (⟨X, .sub δ'⟩ :: (Γ ++ Δ)) := by grind [perm_dlookup]
+    have := @map_val_mem Var (f := ((·[X:=δ]) : Binding Var → Binding Var))
+    by_cases X = X'
+    · trans δ' <;> grind [→ mem_dlookup, Ty.subst_fresh, Ty.Wf.nmem_fv, weaken_head, keys_append]
+    · grind [keys_append]
+  all_goals
+    grind [Env.Wf.to_ok, keys_append, Sub.refl, Env.Wf.map_subst, Ty.Wf.map_subst]
+
+/-- Strengthening of subtypes. -/
+lemma strengthen (sub : Sub (Γ ++ ⟨X, Binding.ty δ⟩ :: Δ) σ τ) :  Sub (Γ ++ Δ) σ τ := by
+  generalize eq : Γ ++ ⟨X, Binding.ty δ⟩ :: Δ = Θ at sub
+  induction sub generalizing Γ 
+  case all => apply Sub.all (free_union Var) <;> grind
+  all_goals grind [to_ok, Wf.strengthen, Env.Wf.strengthen, dlookup_append]
+  
+end Sub
+
+end LambdaCalculus.LocallyNameless.Fsub
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
new file mode 100644
index 00000000..4506b86e
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
@@ -0,0 +1,241 @@
+/-
+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.Languages.LambdaCalculus.LocallyNameless.Fsub.WellFormed
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Subtype
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Reduction
+
+/-! # λ-calculus
+
+The λ-calculus with polymorphism and subtyping, with a locally nameless representation of syntax.
+This file defines the typing relation.
+
+## References
+
+* [A. Chargueraud, *The Locally Nameless Representation*][Chargueraud2012]
+* See also <https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/>, from which
+  this is adapted
+
+-/
+
+variable {Var : Type*} [DecidableEq Var] [HasFresh Var]
+
+namespace LambdaCalculus.LocallyNameless.Fsub
+
+open Term Ty Ty.Wf Env.Wf Sub Context List Binding
+
+/-- The typing relation. -/
+inductive Typing : Env Var → Term Var → Ty Var → Prop
+  | var : Γ.Wf → Binding.ty σ ∈ Γ.dlookup x → Typing Γ (fvar x) σ
+  | abs (L : Finset Var) :
+      (∀ x ∉ L, Typing (⟨x, Binding.ty σ⟩ :: Γ) (t₁ ^ᵗᵗ fvar x) τ) →
+      Typing Γ (abs σ t₁) (arrow σ τ)
+  | app : Typing Γ t₁ (arrow σ τ) → Typing Γ t₂ σ → Typing Γ (app t₁ t₂) τ
+  | tabs (L : Finset Var) :
+      (∀ X ∉ L, Typing (⟨X, Binding.sub σ⟩ :: Γ) (t₁ ^ᵗᵞ fvar X) (τ ^ᵞ fvar X)) →
+      Typing Γ (tabs σ t₁) (all σ τ)
+  | tapp : Typing Γ t₁ (all σ τ) → Sub Γ σ' σ → Typing Γ (tapp t₁ σ') (τ ^ᵞ σ')
+  | sub : Typing Γ t τ → Sub Γ τ τ' → Typing Γ t τ'
+  | let' (L : Finset Var) :
+      Typing Γ t₁ σ →
+      (∀ x ∉ L, Typing (⟨x, Binding.ty σ⟩ :: Γ) (t₂ ^ᵗᵗ fvar x) τ) →
+      Typing Γ (let' t₁ t₂) τ
+  | inl : Typing Γ t₁ σ → τ.Wf Γ → Typing Γ (inl t₁) (sum σ τ)
+  | inr : Typing Γ t₁ τ → σ.Wf Γ → Typing Γ (inr t₁) (sum σ τ)
+  | case (L : Finset Var) :
+      Typing Γ t₁ (sum σ τ) →
+      (∀ x ∉ L, Typing (⟨x, Binding.ty σ⟩ :: Γ) (t₂ ^ᵗᵗ fvar x) δ) →
+      (∀ x ∉ L, Typing (⟨x, Binding.ty τ⟩ :: Γ) (t₃ ^ᵗᵗ fvar x) δ) →
+      Typing Γ (case t₁ t₂ t₃) δ
+
+namespace Typing
+
+variable {Γ Δ Θ : Env Var} {σ τ δ : Ty Var}
+
+attribute [grind] Typing.var Typing.app Typing.tapp Typing.sub Typing.inl Typing.inr
+
+/-- Typings have well-formed contexts and types. -/
+@[grind →]
+lemma wf {Γ : Env Var} {t : Term Var} {τ : Ty Var} (der : Typing Γ t τ) : Γ.Wf ∧ t.LC ∧ τ.Wf Γ := by
+  induction der <;> let L := free_union Var <;> have := fresh_exists L
+  case tabs => refine ⟨?_, LC.tabs L ?_ ?_, Ty.Wf.all L ?_ ?_⟩ <;> grind [cases Env.Wf]
+  case abs => refine ⟨?_, LC.abs L ?_ ?_, ?_⟩ <;> grind [Wf.strengthen, cases Env.Wf]
+  case let' => refine ⟨?_, LC.let' L ?_ ?_, ?_⟩ <;> grind [Ty.Wf.strengthen]
+  case case => refine ⟨?_, LC.case L ?_ ?_ ?_, ?_⟩ <;> grind [Ty.Wf.strengthen]
+  all_goals grind [of_bind_ty, open_lc, cases Env.Wf, cases Ty.Wf]
+
+/-- Weakening of typings. -/
+lemma weaken (der : Typing (Γ ++ Δ) t τ) (wf : (Γ ++ Θ ++ Δ).Wf) : 
+    Typing (Γ ++ Θ ++ Δ) t τ := by
+  generalize eq : Γ ++ Δ = ΓΔ at der
+  induction der generalizing Γ
+  case' abs => apply abs ((Γ ++ Θ ++ Δ).dom ∪ free_union Var)
+  case' tabs => apply tabs ((Γ ++ Θ ++ Δ).dom ∪ free_union Var)
+  case' let' der _ => apply let' ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq)
+  case' case der _ _ => apply case ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq)
+  all_goals 
+    grind [Wf.weaken, Sub.weaken, Wf.of_env_ty, Wf.of_env_sub, Sub.refl, <= sublist_dlookup]
+
+/-- Weakening of typings (at the front). -/
+lemma weaken_head (der : Typing Δ t τ) (wf : (Γ ++ Δ).Wf) :
+    Typing (Γ ++ Δ) t τ := by
+  have eq : Δ = [] ++ Δ := by rfl
+  rw [eq] at der
+  have := Typing.weaken der wf
+  grind
+
+/-- Narrowing of typings. -/
+lemma narrow (sub : Sub Δ δ δ') (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) t τ) :
+    Typing (Γ ++ ⟨X, Binding.sub δ⟩ :: Δ) t τ := by
+  generalize eq : Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ = Θ at der
+  induction der generalizing Γ 
+  case var X' _ _ =>
+    have : X ≠ X' := by grind [→ List.mem_dlookup]
+    have p (δ) : Γ ++ ⟨X, .sub δ⟩ :: Δ ~ ⟨X, .sub δ⟩ :: (Γ ++ Δ) := perm_middle
+    grind [Env.Wf.narrow, List.perm_nodupKeys, => List.perm_dlookup]
+  case' abs  => apply abs (free_union Var)
+  case' tabs => apply tabs (free_union Var)
+  case' let' der _ => apply let' (free_union Var) (der eq)
+  case' case der _ _ => apply case (free_union Var) (der eq)
+  all_goals grind [Ty.Wf.narrow, Env.Wf.narrow, Sub.narrow]
+
+/-- Term substitution within a typing. -/
+lemma subst_tm (der : Typing (Γ ++ ⟨X, .ty σ⟩ :: Δ) t τ) (der_sub : Typing Δ s σ) :
+    Typing (Γ ++ Δ) (t[X := s]) τ := by
+  generalize eq : Γ ++ ⟨X, .ty σ⟩ :: Δ = Θ at der
+  induction der generalizing Γ X
+  case var σ' _ X' _ _ =>
+    have : Γ ++ ⟨X, .ty σ⟩ :: Δ ~ ⟨X, .ty σ⟩ :: (Γ ++ Δ) := perm_middle
+    by_cases eq : X = X'
+    · grind [→ List.mem_dlookup, weaken_head, Env.Wf.strengthen]
+    · grind [Env.Wf.strengthen, => List.perm_dlookup]
+  case abs => 
+    apply abs (free_union Var)
+    grind [open_tm_subst_tm_var]
+  case tabs => 
+    apply tabs (free_union Var)
+    grind [open_ty_subst_tm_var]
+  case let' der _ => 
+    apply let' (free_union Var) (der eq)
+    grind [open_tm_subst_tm_var]
+  case case der _ _ => 
+    apply case (free_union Var) (der eq) <;> grind [open_tm_subst_tm_var]
+  all_goals grind [Env.Wf.strengthen, Ty.Wf.strengthen, Sub.strengthen]
+
+/-- Type substitution within a typing. -/
+lemma subst_ty (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) t τ) (sub : Sub Δ δ δ') : 
+    Typing (Γ.map_val (·[X := δ]) ++ Δ) (t[X := δ]) (τ[X := δ]) := by
+  generalize eq : Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ = Θ at der
+  induction der generalizing Γ X 
+  case var σ _ X' _ mem =>
+    have := map_subst_nmem Δ X δ
+    have : Γ ++ ⟨X, .sub δ'⟩ :: Δ ~ ⟨X, .sub δ'⟩ :: (Γ ++ Δ) := perm_middle
+    have : .ty σ ∈ dlookup X' (⟨X, .sub δ'⟩ :: (Γ ++ Δ)) := by grind [perm_dlookup]
+    have := @map_val_mem Var (f := ((·[X:=δ]) : Binding Var → Binding Var))
+    grind [Env.Wf.map_subst, keys_append, → notMem_keys_of_nodupKeys_cons]
+  case abs => 
+    apply abs (free_union [Ty.fv] Var)
+    grind [Ty.subst_fresh, open_tm_subst_ty_var]
+  case tabs => 
+    apply tabs (free_union Var)
+    grind [open_ty_subst_ty_var, open_subst_var]
+  case let' der _ => 
+    apply let' (free_union Var) (der eq)
+    grind [open_tm_subst_ty_var]
+  case case der _ _ =>
+    apply case (free_union Var) (der eq) <;> grind [open_tm_subst_ty_var]
+  case tapp => grind [Ty.open_subst, Env.Wf.map_subst, Ty.Wf.map_subst, Sub.map_subst]
+  all_goals grind [Env.Wf.map_subst, Ty.Wf.map_subst, Sub.map_subst]
+
+open Term Ty
+
+omit [HasFresh Var]
+
+/-- Invert the typing of an abstraction. -/
+lemma abs_inv (der : Typing Γ (.abs γ' t) τ) (sub : Sub Γ τ (arrow γ δ)) :
+     Sub Γ γ γ'
+  ∧ ∃ δ' L, ∀ x ∉ (L : Finset Var), 
+    Typing (⟨x, Binding.ty γ'⟩ :: Γ) (t ^ᵗᵗ .fvar x) δ' ∧ Sub Γ δ' δ := by
+  generalize eq : Term.abs γ' t = e at der
+  induction der generalizing t γ' γ δ
+  case abs τ L _ _ => 
+    cases eq
+    cases sub
+    split_ands
+    · assumption
+    · exists τ, L
+      grind
+  case sub Γ _ τ τ' _ _ ih => 
+    subst eq
+    have sub' : Sub Γ τ (γ.arrow δ) := by grind
+    obtain ⟨_, δ', L, _⟩ := ih sub' (by rfl)
+    split_ands
+    · assumption
+    · exists δ', L
+  all_goals grind
+
+variable [HasFresh Var] in
+/-- Invert the typing of a type abstraction. -/
+lemma tabs_inv (der : Typing Γ (.tabs γ' t) τ) (sub : Sub Γ τ (all γ δ)) :
+     Sub Γ γ γ'
+  ∧ ∃ δ' L, ∀ X ∉ (L : Finset Var),
+     Typing (⟨X, Binding.sub γ⟩ :: Γ) (t ^ᵗᵞ fvar X) (δ' ^ᵞ fvar X)
+     ∧ Sub (⟨X, Binding.sub γ⟩ :: Γ) (δ' ^ᵞ fvar X) (δ ^ᵞ fvar X) := by
+  generalize eq : Term.tabs γ' t = e at der
+  induction der generalizing γ δ t γ'
+  case tabs σ Γ _ τ L der _ =>
+    cases sub with | all L' sub => 
+    split_ands
+    · grind
+    · exists τ, L ∪ L'
+      intro X _
+      have eq : ⟨X, Binding.sub γ⟩ :: Γ = [] ++ ⟨X, Binding.sub γ⟩ :: Γ := by rfl
+      grind [narrow]
+  case sub Γ _ τ τ' _ _ ih => 
+    subst eq
+    have sub' : Sub Γ τ (γ.all δ) := by trans τ' <;> grind
+    obtain ⟨_, δ', L, _⟩ := ih sub' (by rfl)
+    split_ands
+    · assumption
+    · exists δ', L
+  all_goals grind
+
+/-- Invert the typing of a left case. -/
+lemma inl_inv (der : Typing Γ (.inl t) τ) (sub : Sub Γ τ (sum γ δ)) :
+    ∃ γ', Typing Γ t γ' ∧ Sub Γ γ' γ := by
+  generalize eq : t.inl =t at der
+  induction der generalizing γ δ <;> grind [cases Sub]
+
+/-- Invert the typing of a right case. -/
+lemma inr_inv (der : Typing Γ (.inr t) T) (sub : Sub Γ T (sum γ δ)) :
+    ∃ δ', Typing Γ t δ' ∧ Sub Γ δ' δ := by
+  generalize eq : t.inr =t at der
+  induction der generalizing γ δ <;> grind [cases Sub]
+
+/-- A value that types as a function is an abstraction. -/
+lemma canonical_form_abs (val : Value t) (der : Typing [] t (arrow σ τ)) :
+    ∃ δ t', t = .abs δ t' := by
+  generalize eq  : σ.arrow τ = γ at der
+  generalize eq' : [] = Γ at der
+  induction der generalizing σ τ <;> grind [cases Sub, cases Value]
+
+/-- A value that types as a quantifier is a type abstraction. -/
+lemma canonical_form_tabs (val : Value t) (der : Typing [] t (all σ τ)) :
+    ∃ δ t', t = .tabs δ t' := by
+  generalize eq  : σ.all τ = γ at der
+  generalize eq' : [] = Γ at der
+  induction der generalizing σ τ <;> grind [cases Sub, cases Value]
+
+/-- A value that types as a sum is a left or right case. -/
+lemma canonical_form_sum (val : Value t) (der : Typing [] t (sum σ τ)) :
+    ∃ t', t = .inl t' ∨ t = .inr t' := by
+  generalize eq  : σ.sum τ = γ at der
+  generalize eq' : [] = Γ at der
+  induction der generalizing σ τ <;> grind [cases Sub, cases Value]
+
+end Typing
+
+end LambdaCalculus.LocallyNameless.Fsub
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean
new file mode 100644
index 00000000..a50694f1
--- /dev/null
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/WellFormed.lean
@@ -0,0 +1,188 @@
+/-
+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.Languages.LambdaCalculus.LocallyNameless.Fsub.Basic
+import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Opening
+
+/-! # λ-calculus
+
+The λ-calculus with polymorphism and subtyping, with a locally nameless representation of syntax.
+This file defines the well-formedness condition for types and contexts.
+
+## References
+
+* [A. Chargueraud, *The Locally Nameless Representation*][Chargueraud2012]
+* See also <https://www.cis.upenn.edu/~plclub/popl08-tutorial/code/>, from which
+  this is adapted
+
+-/
+
+variable {Var : Type*} [DecidableEq Var]
+
+namespace LambdaCalculus.LocallyNameless.Fsub
+
+open scoped Ty in
+/-- A type is well-formed when it is locally closed and all free variables appear in a context. -/
+inductive Ty.Wf : Env Var → Ty Var → Prop
+  | top : Ty.Wf Γ top
+  | var : Binding.sub σ ∈ Γ.dlookup X → Ty.Wf Γ (fvar X)
+  | arrow : Ty.Wf Γ σ → Ty.Wf Γ τ → Ty.Wf Γ (arrow σ τ)
+  | all (L : Finset Var) : 
+      Ty.Wf Γ σ →
+      (∀ X ∉ L, Ty.Wf (⟨X,Binding.sub σ⟩ :: Γ) (τ ^ᵞ fvar X)) →
+      Ty.Wf Γ (all σ τ)
+  | sum : Ty.Wf Γ σ → Ty.Wf Γ τ → Ty.Wf Γ (sum σ τ)
+
+attribute [scoped grind] Ty.Wf.top Ty.Wf.var Ty.Wf.arrow Ty.Wf.sum
+
+/-- An environment is well-formed if it binds each variable exactly once to a well-formed type. -/
+inductive Env.Wf : Env Var → Prop
+  | empty : Wf []
+  | sub : Wf Γ → τ.Wf Γ → X ∉ Γ.dom → Wf (⟨X, Binding.sub τ⟩ :: Γ)
+  | ty : Wf Γ → τ.Wf Γ → x ∉ Γ.dom → Wf (⟨x, Binding.ty τ⟩ :: Γ)
+
+attribute [scoped grind] Env.Wf.sub Env.Wf.ty
+
+variable {Γ Δ Θ : Env Var} {σ τ τ' γ δ : Ty Var}
+
+open scoped Context in
+/-- A well-formed context contains no duplicate keys. -/
+@[scoped grind →]
+lemma Env.Wf.to_ok {Γ : Env Var} (wf : Γ.Wf) : Γ✓ := by
+  induction wf <;> constructor <;> first | assumption | grind [List.mem_keys_of_mem]
+
+namespace Ty.Wf
+
+open Context List Binding
+open scoped Env.Wf
+
+/-- A well-formed type is locally closed. -/
+@[grind →]
+theorem lc (wf : σ.Wf Γ) : σ.LC := by
+  induction wf with
+  | all => apply LC.all (free_union Var) <;> grind
+  | _ => grind
+
+/-- A type remains well-formed under context permutation. -/
+theorem perm_env (wf : σ.Wf Γ) (perm : Γ ~ Δ) (ok_Γ : Γ✓) (ok_Δ : Δ✓) : σ.Wf Δ := by
+  induction wf generalizing Δ with
+  | all => apply all (free_union [dom] Var) <;> grind [Perm.cons, nodupKeys_cons]
+  | _ => grind [perm_dlookup]
+
+/-- A type remains well-formed under context weakening (in the middle). -/
+theorem weaken (wf_ΓΘ : σ.Wf (Γ ++ Θ)) (ok_ΓΔΘ : (Γ ++ Δ ++ Θ)✓) : σ.Wf (Γ ++ Δ ++ Θ) := by
+  generalize eq : Γ ++ Θ = ΓΔ at wf_ΓΘ
+  induction wf_ΓΘ generalizing Γ
+  case all => apply all ((Γ ++ Δ ++ Θ).dom ∪ free_union Var) <;> grind
+  all_goals grind [NodupKeys.sublist, <= sublist_dlookup]
+
+/-- A type remains well-formed under context weakening (at the front). -/
+theorem weaken_head (wf : σ.Wf Δ) (ok : (Γ ++ Δ)✓) : σ.Wf (Γ ++ Δ) := by
+  have : Γ ++ Δ = [] ++ Γ ++ Δ := by rfl
+  grind [weaken]
+
+theorem weaken_cons (wf : σ.Wf Δ) (ok : (⟨X, b⟩ :: Δ)✓) : σ.Wf (⟨X, b⟩:: Δ) := by
+  grind [weaken_head]
+
+/-- A type remains well-formed under context narrowing. -/
+lemma narrow (wf : σ.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (ok : (Γ ++ ⟨X, Binding.sub τ'⟩ :: Δ)✓) :
+    σ.Wf (Γ ++ ⟨X, Binding.sub τ'⟩ :: Δ) := by
+  generalize eq : (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ) = Θ at wf
+  induction wf generalizing Γ with
+  | all => apply all (free_union [dom] Var) <;> grind [nodupKeys_cons, keys_append]
+  | _ => grind [sublist_dlookup, dlookup_append]
+
+lemma narrow_cons (wf : σ.Wf (⟨X, Binding.sub τ⟩ :: Δ)) (ok : (⟨X, Binding.sub τ'⟩ :: Δ)✓) :
+    σ.Wf (⟨X, Binding.sub τ'⟩ :: Δ) := by
+  rw [←List.nil_append (⟨X, sub τ'⟩ :: Δ)]
+  grind [narrow]
+
+/-- A type remains well-formed under context strengthening. -/
+lemma strengthen (wf : σ.Wf (Γ ++ ⟨X, Binding.ty τ⟩ :: Δ)) : σ.Wf (Γ ++ Δ) := by
+  generalize eq : Γ ++ ⟨X, Binding.ty τ⟩ :: Δ = Θ at wf
+  induction wf generalizing Γ with
+  | all => apply all (free_union [Context.dom] Var) <;> grind
+  | _ => grind [dlookup_append]
+
+variable [HasFresh Var] in
+/-- A type remains well-formed under context substitution (of a well-formed type). -/
+lemma map_subst (wf_σ : σ.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (wf_τ' : τ'.Wf Δ)
+    (ok : (Γ.map_val (·[X:=τ']) ++ Δ)✓) : σ[X:=τ'].Wf <| Γ.map_val (·[X:=τ']) ++ Δ := by
+  have := @map_val_mem Var (Binding Var)      
+  generalize eq : Γ ++ ⟨X, Binding.sub τ⟩ :: Δ = Θ at wf_σ
+  induction wf_σ generalizing Γ τ'
+  case all γ _ _ _ _ _ _ => 
+    subst eq
+    apply all (free_union [dom] Var)
+    · grind
+    · intro X' _
+      have : (map_val (·[X:=τ']) (⟨X', Binding.sub γ⟩ :: Γ) ++ Δ)✓ := by grind [keys_append]
+      grind [open_subst_var]
+  all_goals grind [weaken_head, dlookup_append]
+
+variable [HasFresh Var] in
+/-- A type remains well-formed under opening (to a well-formed type). -/
+lemma open_lc (ok_Γ : Γ✓) (wf_all : (Ty.all σ τ).Wf Γ) (wf_δ : δ.Wf Γ) : (τ ^ᵞ δ).Wf Γ := by
+  cases wf_all with | all => 
+    let ⟨X, _⟩ := fresh_exists <| free_union [fv, Context.dom] Var
+    have : Γ = Context.map_val (·[X:=δ]) [] ++ Γ := by grind
+    grind [open_subst_intro, map_subst]
+
+/-- A type bound in a context is well formed. -/
+lemma of_bind_ty (wf : Γ.Wf) (bind : Binding.ty σ ∈ Γ.dlookup X) : σ.Wf Γ := by
+  induction wf <;> grind [weaken_head]
+
+/-- A type at the head of a well-formed context is well-formed. -/
+lemma of_env_ty (wf : Env.Wf (⟨X, Binding.ty σ⟩ :: Γ)) : σ.Wf Γ := by
+  cases wf
+  assumption
+
+/-- A subtype at the head of a well-formed context is well-formed. -/
+lemma of_env_sub (wf : Env.Wf (⟨X, Binding.sub σ⟩ :: Γ)) : σ.Wf Γ := by
+  cases wf
+  assumption
+
+variable [HasFresh Var] in
+/-- A variable not appearing in a context does not appear in its well-formed types. -/
+lemma nmem_fv {σ : Ty Var} (wf : σ.Wf Γ) (nmem : X ∉ Γ.dom) : X ∉ σ.fv := by
+  induction wf with
+  | all => have := fresh_exists <| free_union [dom] Var; grind [nmem_fv_open, openRec_lc]
+  | _ => grind
+
+end Ty.Wf
+
+namespace Env.Wf
+
+open Context List Binding
+
+/-- A context remains well-formed under narrowing (of a well-formed subtype). -/
+lemma narrow (wf_env : Env.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (wf_τ' : τ'.Wf Δ) : 
+    Env.Wf (Γ ++ ⟨X, Binding.sub τ'⟩ :: Δ) := by
+  induction Γ <;> cases wf_env <;> 
+  grind [Ty.Wf.narrow, keys_append, eq_nil_of_append_eq_nil, cases Env.Wf]
+      
+/-- A context remains well-formed under strengthening. -/
+lemma strengthen (wf : Env.Wf <| Γ ++ ⟨X, Binding.ty τ⟩ :: Δ) : Env.Wf <| Γ ++ Δ := by
+  induction Γ <;> cases wf <;> grind [Ty.Wf.strengthen, keys_append]
+
+variable [HasFresh Var] in
+/-- A context remains well-formed under substitution (of a well-formed type). -/
+lemma map_subst (wf_env : Env.Wf (Γ ++ ⟨X, Binding.sub τ⟩ :: Δ)) (wf_τ' : τ'.Wf Δ) :
+    Env.Wf <| Γ.map_val (·[X:=τ']) ++ Δ := by
+  induction Γ generalizing wf_τ' Δ τ' <;> cases wf_env
+  case nil => grind
+  case cons.sub | cons.ty => constructor <;> grind [Ty.Wf.map_subst, keys_append]
+    
+variable [HasFresh Var]
+
+/-- A well-formed context is unchaged by substituting for a free key. -/
+lemma map_subst_nmem (Γ : Env Var) (X : Var) (σ : Ty Var) (wf : Γ.Wf) (nmem : X ∉ Γ.dom) :
+    Γ = Γ.map_val (·[X:=σ]) := by
+  induction wf <;> grind [Ty.Wf.nmem_fv, Binding.subst_fresh]
+
+end Env.Wf
+    
+end LambdaCalculus.LocallyNameless.Fsub
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Basic.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
index 5e28a18f..016f5e02 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Basic.lean
@@ -102,7 +102,7 @@ lemma subst_aux (h : Δ ++ ⟨x, σ⟩ :: Γ ⊢ t ∶ τ) (der : Γ ⊢ s ∶ 
   case var x' τ ok mem => 
     simp only [subst_fvar]
     subst eq
-    cases (Context.wf_perm (by simp) ok : (⟨x, σ⟩ :: Δ ++ Γ)✓)
+    cases ((List.perm_nodupKeys (by simp)).mp ok : (⟨x, σ⟩ :: Δ ++ Γ)✓)
     case cons ok_weak _ =>
     observe perm : (Γ ++ Δ).Perm (Δ ++ Γ)
     by_cases h : x = x' <;> simp only [h]
@@ -120,7 +120,7 @@ lemma subst_aux (h : Δ ++ ⟨x, σ⟩ :: Γ ⊢ t ∶ τ) (der : Γ ⊢ s ∶ 
         match mem with | _ => simp_all
       rw [eq']
       refine (weaken der ?_).perm perm
-      exact Context.wf_perm (id (List.Perm.symm perm)) ok_weak
+      grind
   case abs σ Γ' t T2 xs ih' ih =>
     apply Typing.abs (free_union Var)
     intros