From bd4d3039befb399bf375cf28b6c78a9d0ebf3275 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sat, 21 Mar 2026 07:38:42 -0400
Subject: [PATCH 01/14] try a grind only

---
 .../LambdaCalculus/LocallyNameless/Fsub/Typing.lean         | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
index 9743f2ab4..60c7062df 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
@@ -11,6 +11,8 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Subtype
 
 @[expose] public section
 
+--set_option trace.profiler.useHeartbeats true
+
 /-! # λ-calculus
 
 The λ-calculus with polymorphism and subtyping, with a locally nameless representation of syntax.
@@ -234,7 +236,9 @@ 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]
+  induction der generalizing σ τ with
+  | sub _ s => cases s <;> grind only [= Option.mem_def, = dlookup_nil]
+  | _ => grind only [= Option.mem_def, = dlookup_nil]
 
 end Typing
 

From 0b8638bcf7e5696a2c0d1717ebc5bbcb58c270b1 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sat, 21 Mar 2026 07:51:19 -0400
Subject: [PATCH 02/14] inversion

---
 .../LocallyNameless/Fsub/Typing.lean          | 23 +++++++++++++++----
 1 file changed, 18 insertions(+), 5 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
index 60c7062df..61fb1df6c 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
@@ -209,27 +209,39 @@ lemma tabs_inv (der : Typing Γ (.tabs γ' t) τ) (sub : Sub Γ τ (all γ δ))
 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]
+  induction der generalizing γ δ with
+  | inl => cases sub; grind only
+  | sub => grind only [→ Sub.trans]
+  | _ => grind only
 
 /-- 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]
+  induction der generalizing γ δ with
+  | inr => cases sub; grind only
+  | sub => grind only [→ Sub.trans]
+  | _ => grind only
 
 /-- 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]
+  induction der generalizing σ τ with
+  | sub _ s => cases s <;> grind only [= Option.mem_def, = dlookup_nil]
+  | var => grind only [= Option.mem_def, = dlookup_nil]
+  | _ => grind only
 
 /-- 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]
+  induction der generalizing σ τ with
+  | sub _ s => cases s <;> grind only [= Option.mem_def, = dlookup_nil]
+  | var => grind only [= Option.mem_def, = dlookup_nil]
+  | _ => grind only
 
 /-- A value that types as a sum is a left or right case. -/
 lemma canonical_form_sum (val : Value t) (der : Typing [] t (sum σ τ)) :
@@ -238,7 +250,8 @@ lemma canonical_form_sum (val : Value t) (der : Typing [] t (sum σ τ)) :
   generalize eq' : [] = Γ at der
   induction der generalizing σ τ with
   | sub _ s => cases s <;> grind only [= Option.mem_def, = dlookup_nil]
-  | _ => grind only [= Option.mem_def, = dlookup_nil]
+  | var => grind only [= Option.mem_def, = dlookup_nil]
+  | _ => grind only
 
 end Typing
 

From 8f9059b55aa88c766040cd112c259c572b1e90f1 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sat, 21 Mar 2026 08:21:05 -0400
Subject: [PATCH 03/14] tabs_inv

---
 .../LocallyNameless/Fsub/Typing.lean          | 34 +++++++++----------
 1 file changed, 17 insertions(+), 17 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
index 61fb1df6c..567074b12 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
@@ -187,23 +187,23 @@ lemma tabs_inv (der : Typing Γ (.tabs γ' t) τ) (sub : Sub Γ τ (all γ δ))
      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 _ =>
+  induction der generalizing γ δ t γ' with
+  | @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
+    cases eq
+    use sub, τ, L ∪ L'
+    intro X _
+    have eq : ⟨X, .sub γ⟩ :: Γ = [] ++ ⟨X, .sub γ⟩ :: Γ := rfl
+    grind only [= Finset.mem_union, narrow]
+  | sub _ sub_τ ih => exact ih (sub_τ.trans sub) eq
+  | var => grind only
+  | abs => grind only
+  | app => grind only
+  | tapp => grind only
+  | let' => grind only
+  | inl => grind only
+  | inr => grind only
+  | case => grind only
 
 /-- Invert the typing of a left case. -/
 lemma inl_inv (der : Typing Γ (.inl t) τ) (sub : Sub Γ τ (sum γ δ)) :
@@ -217,7 +217,7 @@ lemma inl_inv (der : Typing Γ (.inl t) τ) (sub : Sub Γ τ (sum γ δ)) :
 /-- 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
+  generalize eq : t.inr = t at der
   induction der generalizing γ δ with
   | inr => cases sub; grind only
   | sub => grind only [→ Sub.trans]

From 3ab3ffa11e5d8a2090f59a919422e48de95db28b Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sat, 21 Mar 2026 08:38:09 -0400
Subject: [PATCH 04/14] abs_inv

---
 .../LocallyNameless/Fsub/Typing.lean          | 22 ++++++-------------
 1 file changed, 7 insertions(+), 15 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
index 567074b12..6ad9cbe6b 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
@@ -162,22 +162,14 @@ lemma abs_inv (der : Typing Γ (.abs γ' t) τ) (sub : Sub Γ τ (arrow γ δ))
   ∧ ∃ δ' 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 _ _ =>
+  induction der generalizing t γ' γ δ with
+  | @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
+    cases sub with | arrow sub_γ =>
+    use sub_γ, τ, L
+    grind
+  | sub _ sub_τ ih => exact ih (sub_τ.trans sub) eq
+  | _ => grind only
 
 variable [HasFresh Var] in
 /-- Invert the typing of a type abstraction. -/

From 59e46f9ebf891268423a5f970ec651cb021aeb3b Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sat, 21 Mar 2026 08:42:57 -0400
Subject: [PATCH 05/14] weaken_head

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

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
index 6ad9cbe6b..66d139b5c 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
@@ -91,11 +91,10 @@ lemma weaken (der : Typing (Γ ++ Δ) t τ) (wf : (Γ ++ Θ ++ Δ).Wf) :
     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
+lemma weaken_head (der : Typing Δ t τ) (wf : (Γ ++ Δ).Wf) : Typing (Γ ++ Δ) t τ := by
+  have eq : Δ = [] ++ Δ := rfl
   rw [eq] at der
-  grind [Typing.weaken der wf]
+  exact der.weaken wf
 
 /-- Narrowing of typings. -/
 lemma narrow (sub : Sub Δ δ δ') (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) t τ) :

From 709183eb28c30746e510403287f5a3f6172e4d75 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sat, 21 Mar 2026 19:17:23 -0400
Subject: [PATCH 06/14] squeeze var case of subst_ty, explicit case split

---
 .../LocallyNameless/Fsub/Typing.lean            | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
index 66d139b5c..e8878c97a 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
@@ -138,9 +138,24 @@ lemma subst_ty (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) t τ) (sub :
   generalize eq : Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ = Θ at der
   induction der generalizing Γ X
   case var σ _ X' _ mem =>
+    expose_names
     have := map_subst_nmem Δ X δ
     have := @map_val_mem Var (f := ((·[X:=δ]) : Binding Var → Binding Var))
-    grind [Env.Wf.map_subst, → notMem_keys_of_nodupKeys_cons]
+    have := sub.wf
+    -- could split this interactively??
+    by_cases h : X = X'
+    · have : (Term.fvar X')[X:=δ] = Term.fvar X' := rfl
+      rw [this]
+      constructor
+      · grind only [!Env.Wf.map_subst]
+      · grind only [= Option.mem_def, = Binding.subst_ty, = dlookup_append, = Option.or_eq_some_iff,
+          = dlookup_cons_eq]
+    · constructor
+      · grind only [!Env.Wf.map_subst]
+      · grind only [→ to_ok, = dom, = map_val, = Binding.subst_ty,
+        = haswellformed_def, = mem_toFinset, = dlookup_append, = map_append,
+        = nodupKeys_middle, → notMem_keys_of_nodupKeys_cons,
+        = map_cons, = dlookup_cons_ne, = keys_append, = mem_append]
   case abs => grind [abs (free_union [Ty.fv] Var), Ty.subst_fresh, open_tm_subst_ty_var]
   case tabs => grind [tabs (free_union Var), open_ty_subst_ty_var, open_subst_var]
   case let' der _ =>

From 8347f3672e391f8bde675444487ca5b98c120fb0 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sat, 21 Mar 2026 19:39:35 -0400
Subject: [PATCH 07/14] a bit more restructure...

---
 .../LocallyNameless/Fsub/Typing.lean          | 22 +++++++++++--------
 1 file changed, 13 insertions(+), 9 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
index e8878c97a..28dd5c762 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
@@ -138,24 +138,28 @@ lemma subst_ty (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) t τ) (sub :
   generalize eq : Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ = Θ at der
   induction der generalizing Γ X
   case var σ _ X' _ mem =>
-    expose_names
-    have := map_subst_nmem Δ X δ
     have := @map_val_mem Var (f := ((·[X:=δ]) : Binding Var → Binding Var))
+    have : X = X' ∨ ¬ X = X' := Decidable.eq_or_ne X X'
     have := sub.wf
     -- could split this interactively??
     by_cases h : X = X'
-    · have : (Term.fvar X')[X:=δ] = Term.fvar X' := rfl
-      rw [this]
-      constructor
+    · constructor
       · grind only [!Env.Wf.map_subst]
       · grind only [= Option.mem_def, = Binding.subst_ty, = dlookup_append, = Option.or_eq_some_iff,
           = dlookup_cons_eq]
     · constructor
       · grind only [!Env.Wf.map_subst]
-      · grind only [→ to_ok, = dom, = map_val, = Binding.subst_ty,
-        = haswellformed_def, = mem_toFinset, = dlookup_append, = map_append,
-        = nodupKeys_middle, → notMem_keys_of_nodupKeys_cons,
-        = map_cons, = dlookup_cons_ne, = keys_append, = mem_append]
+      · expose_names
+        subst eq
+        have := h_1.to_ok
+        have : Δ = map_val (fun x => x[X:=δ]) Δ := by 
+          apply map_subst_nmem Δ X δ
+          · grind only
+          · grind only [= haswellformed_def, = dom,
+            = NodupKeys, = mem_toFinset, = keys_append, = keys_cons,
+            = nodup_append, = nodup_cons]
+        grind only [= map_val, = Binding.subst_ty, = dlookup_append, = map_append, = map_cons,
+          = dlookup_cons_ne]
   case abs => grind [abs (free_union [Ty.fv] Var), Ty.subst_fresh, open_tm_subst_ty_var]
   case tabs => grind [tabs (free_union Var), open_ty_subst_ty_var, open_subst_var]
   case let' der _ =>

From d02759b3d89e3aea8ebfba71209044e1fe50fb4b Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sat, 21 Mar 2026 19:46:35 -0400
Subject: [PATCH 08/14] ws

---
 Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
index 28dd5c762..0cf36664b 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
@@ -152,7 +152,7 @@ lemma subst_ty (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩ :: Δ) t τ) (sub :
       · expose_names
         subst eq
         have := h_1.to_ok
-        have : Δ = map_val (fun x => x[X:=δ]) Δ := by 
+        have : Δ = map_val (fun x => x[X:=δ]) Δ := by
           apply map_subst_nmem Δ X δ
           · grind only
           · grind only [= haswellformed_def, = dom,

From 71c54585de34f86793ebc390a4e2ce98d6952070 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 22 Mar 2026 02:51:48 -0400
Subject: [PATCH 09/14] squeeze var case a bit harder

---
 .../LocallyNameless/Fsub/Typing.lean          | 21 +++++++++++--------
 1 file changed, 12 insertions(+), 9 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
index 0cf36664b..04ef475a4 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
@@ -114,16 +114,19 @@ lemma subst_tm (der : Typing (Γ ++ ⟨X, .ty σ⟩ :: Δ) t τ) (der_sub : Typi
     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
+  case var σ' _ X' wf _ =>
     by_cases eq : X = X'
-    · #adaptation_note
-      /--
-      Moving from `nightly-2025-09-15` to `nightly-2025-10-19`,
-      I've had to remove the `append_assoc` lemma from grind;
-      without this `grind` is exploding. This requires further investigation.
-      -/
-      grind [→ List.mem_dlookup, weaken_head, Env.Wf.strengthen, -append_assoc]
+    · subst eq
+      subst eq
+      have : Γ ++ ⟨X, .ty σ⟩ :: Δ ~ ⟨X, .ty σ⟩ :: (Γ ++ Δ) := perm_middle
+      have := List.perm_dlookup X wf.to_ok this
+      have : Binding.ty σ' ∈ dlookup X (⟨X, Binding.ty σ⟩ :: (Γ ++ Δ)) := by grind only
+      have : σ = σ' := by grind only [= Option.mem_def, = dlookup_cons_eq]
+      subst this
+      have : (Term.fvar X)[X:=s] = s := by grind only [=_ subst_tm_def, = subst_tm.eq_2]
+      rw [this]
+      apply weaken_head der_sub
+      grind only [!Env.Wf.strengthen]
     · grind [Env.Wf.strengthen, => List.perm_dlookup]
   case abs => grind [abs (free_union Var), open_tm_subst_tm_var]
   case tabs => grind [tabs (free_union Var), open_ty_subst_tm_var]

From ee8f59fbdf5948001256933a89fd32bf0f209161 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 22 Mar 2026 03:06:33 -0400
Subject: [PATCH 10/14] try interactive mode

---
 .../LocallyNameless/Fsub/Typing.lean          | 27 +++++++++----------
 1 file changed, 12 insertions(+), 15 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
index 04ef475a4..d88594c20 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
@@ -112,27 +112,24 @@ lemma narrow (sub : Sub Δ δ δ') (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩
 /-- 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
+  generalize eq₁ : Γ ++ ⟨X, .ty σ⟩ :: Δ = Θ at der
   induction der generalizing Γ X
   case var σ' _ X' wf _ =>
-    by_cases eq : X = X'
-    · subst eq
-      subst eq
-      have : Γ ++ ⟨X, .ty σ⟩ :: Δ ~ ⟨X, .ty σ⟩ :: (Γ ++ Δ) := perm_middle
-      have := List.perm_dlookup X wf.to_ok this
-      have : Binding.ty σ' ∈ dlookup X (⟨X, Binding.ty σ⟩ :: (Γ ++ Δ)) := by grind only
-      have : σ = σ' := by grind only [= Option.mem_def, = dlookup_cons_eq]
-      subst this
-      have : (Term.fvar X)[X:=s] = s := by grind only [=_ subst_tm_def, = subst_tm.eq_2]
-      rw [this]
-      apply weaken_head der_sub
-      grind only [!Env.Wf.strengthen]
+    by_cases eq₂ : X = X'
+    · subst eq₁ eq₂
+      have := weaken_head der_sub wf.strengthen
+      have perm : Γ ++ ⟨X, .ty σ⟩ :: Δ ~ ⟨X, .ty σ⟩ :: (Γ ++ Δ) := perm_middle
+      grind =>
+        have := List.perm_dlookup X wf.to_ok perm
+        have : .ty σ' ∈ dlookup X (⟨X, .ty σ⟩ :: (Γ ++ Δ))
+        have : σ = σ'
+        finish
     · grind [Env.Wf.strengthen, => List.perm_dlookup]
   case abs => grind [abs (free_union Var), open_tm_subst_tm_var]
   case tabs => grind [tabs (free_union Var), open_ty_subst_tm_var]
-  case let' der _ => grind [let' (free_union Var) (der eq), open_tm_subst_tm_var]
+  case let' der _ => grind [let' (free_union Var) (der eq₁), open_tm_subst_tm_var]
   case case der _ _ =>
-    apply case (free_union Var) (der eq) <;> grind [open_tm_subst_tm_var]
+    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. -/

From 736d1a472775c9eef4c6416f9577f89b3a300854 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 22 Mar 2026 03:12:11 -0400
Subject: [PATCH 11/14] see how much unification matters

---
 .../LocallyNameless/Fsub/Typing.lean               | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
index d88594c20..56c4039f0 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
@@ -119,15 +119,21 @@ lemma subst_tm (der : Typing (Γ ++ ⟨X, .ty σ⟩ :: Δ) t τ) (der_sub : Typi
     · subst eq₁ eq₂
       have := weaken_head der_sub wf.strengthen
       have perm : Γ ++ ⟨X, .ty σ⟩ :: Δ ~ ⟨X, .ty σ⟩ :: (Γ ++ Δ) := perm_middle
+      have := List.perm_dlookup X wf.to_ok perm
       grind =>
-        have := List.perm_dlookup X wf.to_ok perm
         have : .ty σ' ∈ dlookup X (⟨X, .ty σ⟩ :: (Γ ++ Δ))
         have : σ = σ'
         finish
     · grind [Env.Wf.strengthen, => List.perm_dlookup]
-  case abs => grind [abs (free_union Var), open_tm_subst_tm_var]
-  case tabs => grind [tabs (free_union Var), open_ty_subst_tm_var]
-  case let' der _ => grind [let' (free_union Var) (der eq₁), open_tm_subst_tm_var]
+  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]

From e8df3b486f14be740bbc3dc4d73caf5ac3efc25e Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 22 Mar 2026 05:31:10 -0400
Subject: [PATCH 12/14] some harmless cases

---
 .../LocallyNameless/Fsub/Typing.lean          | 48 +++++++------------
 1 file changed, 18 insertions(+), 30 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
index 56c4039f0..05b95a47f 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
@@ -92,8 +92,7 @@ lemma weaken (der : Typing (Γ ++ Δ) t τ) (wf : (Γ ++ Θ ++ Δ).Wf) :
 
 /-- Weakening of typings (at the front). -/
 lemma weaken_head (der : Typing Δ t τ) (wf : (Γ ++ Δ).Wf) : Typing (Γ ++ Δ) t τ := by
-  have eq : Δ = [] ++ Δ := rfl
-  rw [eq] at der
+  change Typing ([] ++ Δ) t τ at der
   exact der.weaken wf
 
 /-- Narrowing of typings. -/
@@ -118,8 +117,7 @@ lemma subst_tm (der : Typing (Γ ++ ⟨X, .ty σ⟩ :: Δ) t τ) (der_sub : Typi
     by_cases eq₂ : X = X'
     · subst eq₁ eq₂
       have := weaken_head der_sub wf.strengthen
-      have perm : Γ ++ ⟨X, .ty σ⟩ :: Δ ~ ⟨X, .ty σ⟩ :: (Γ ++ Δ) := perm_middle
-      have := List.perm_dlookup X wf.to_ok perm
+      have := List.perm_dlookup X wf.to_ok perm_middle
       grind =>
         have : .ty σ' ∈ dlookup X (⟨X, .ty σ⟩ :: (Γ ++ Δ))
         have : σ = σ'
@@ -193,7 +191,7 @@ lemma abs_inv (der : Typing Γ (.abs γ' t) τ) (sub : Sub Γ τ (arrow γ δ))
     use sub_γ, τ, L
     grind
   | sub _ sub_τ ih => exact ih (sub_τ.trans sub) eq
-  | _ => grind only
+  | _ => grind
 
 variable [HasFresh Var] in
 /-- Invert the typing of a type abstraction. -/
@@ -209,35 +207,28 @@ lemma tabs_inv (der : Typing Γ (.tabs γ' t) τ) (sub : Sub Γ τ (all γ δ))
     cases eq
     use sub, τ, L ∪ L'
     intro X _
-    have eq : ⟨X, .sub γ⟩ :: Γ = [] ++ ⟨X, .sub γ⟩ :: Γ := rfl
-    grind only [= Finset.mem_union, narrow]
+    split_ands
+    · have eq : ⟨X, .sub γ⟩ :: Γ = [] ++ ⟨X, .sub γ⟩ :: Γ := rfl
+      grind only [= Finset.mem_union, narrow]
+    · grind
   | sub _ sub_τ ih => exact ih (sub_τ.trans sub) eq
-  | var => grind only
-  | abs => grind only
-  | app => grind only
-  | tapp => grind only
-  | let' => grind only
-  | inl => grind only
-  | inr => grind only
-  | case => grind only
+  | _ => 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 γ δ with
-  | inl => cases sub; grind only
-  | sub => grind only [→ Sub.trans]
-  | _ => grind only
+  | inl => cases sub; grind
+  | _ => grind
 
 /-- 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 γ δ with
-  | inr => cases sub; grind only
-  | sub => grind only [→ Sub.trans]
-  | _ => grind only
+  | inr => cases sub; grind
+  | _ => grind
 
 /-- A value that types as a function is an abstraction. -/
 lemma canonical_form_abs (val : Value t) (der : Typing [] t (arrow σ τ)) :
@@ -245,9 +236,8 @@ lemma canonical_form_abs (val : Value t) (der : Typing [] t (arrow σ τ)) :
   generalize eq  : σ.arrow τ = γ at der
   generalize eq' : [] = Γ at der
   induction der generalizing σ τ with
-  | sub _ s => cases s <;> grind only [= Option.mem_def, = dlookup_nil]
-  | var => grind only [= Option.mem_def, = dlookup_nil]
-  | _ => grind only
+  | sub _ s => cases s <;> grind
+  | _ => grind
 
 /-- A value that types as a quantifier is a type abstraction. -/
 lemma canonical_form_tabs (val : Value t) (der : Typing [] t (all σ τ)) :
@@ -255,9 +245,8 @@ lemma canonical_form_tabs (val : Value t) (der : Typing [] t (all σ τ)) :
   generalize eq  : σ.all τ = γ at der
   generalize eq' : [] = Γ at der
   induction der generalizing σ τ with
-  | sub _ s => cases s <;> grind only [= Option.mem_def, = dlookup_nil]
-  | var => grind only [= Option.mem_def, = dlookup_nil]
-  | _ => grind only
+  | sub _ s => cases s <;> grind
+  | _ => grind
 
 /-- A value that types as a sum is a left or right case. -/
 lemma canonical_form_sum (val : Value t) (der : Typing [] t (sum σ τ)) :
@@ -265,9 +254,8 @@ lemma canonical_form_sum (val : Value t) (der : Typing [] t (sum σ τ)) :
   generalize eq  : σ.sum τ = γ at der
   generalize eq' : [] = Γ at der
   induction der generalizing σ τ with
-  | sub _ s => cases s <;> grind only [= Option.mem_def, = dlookup_nil]
-  | var => grind only [= Option.mem_def, = dlookup_nil]
-  | _ => grind only
+  | sub _ s => cases s <;> grind
+  | _ => grind
 
 end Typing
 

From c331b8d3c6c19e671d73b565f92b108cfc20b398 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 22 Mar 2026 09:19:59 -0400
Subject: [PATCH 13/14] more splitting of rules, weirdness in context
 middles...

---
 .../LocallyNameless/Fsub/Typing.lean          | 59 ++++++++++++++-----
 1 file changed, 44 insertions(+), 15 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
index 05b95a47f..c4fc11066 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
@@ -82,13 +82,28 @@ lemma wf {Γ : Env Var} {t : Term Var} {τ : Ty Var} (der : Typing Γ t τ) : Γ
 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]
+  induction der generalizing Γ with
+  | abs =>
+    apply abs ((Γ ++ Θ ++ Δ).dom ∪ free_union Var)
+    grind [Wf.weaken, Wf.of_env_ty]
+  | tabs => 
+    apply tabs ((Γ ++ Θ ++ Δ).dom ∪ free_union Var)
+    grind [Wf.weaken, Wf.of_env_sub]
+  | let' _ _ _ der =>
+    apply let' ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq)
+    grind
+  | case _ _ _ _ der => 
+    apply case ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq)
+    · grind [Wf.weaken, Wf.of_env_ty]
+    · grind [Wf.weaken, Wf.of_env_ty]
+  | var => grind [<= sublist_dlookup]
+  | app => grind
+  | tapp => grind [Sub.weaken]
+  | inl => 
+    -- TODO: break this and look at the way it's extending the context in the middle
+    grind [Sub.weaken, Sub.refl]
+  | inr => grind [Sub.weaken, Sub.refl]
+  | sub => grind [Sub.weaken]
 
 /-- Weakening of typings (at the front). -/
 lemma weaken_head (der : Typing Δ t τ) (wf : (Γ ++ Δ).Wf) : Typing (Γ ++ Δ) t τ := by
@@ -99,14 +114,28 @@ lemma weaken_head (der : Typing Δ t τ) (wf : (Γ ++ Δ).Wf) : Typing (Γ ++ Δ
 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' _ _ =>
-    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]
+  induction der generalizing Γ with
+  | var =>
+    -- TODO: split manually??
+    grind [Env.Wf.narrow]
+  | abs  => 
+    apply abs (free_union Var)
+    grind
+  | tabs => 
+    apply tabs (free_union Var)
+    grind
+  | let' _ _ _ der => 
+    apply let' (free_union Var) (der eq)
+    grind
+  | case _ _ _ _ der => 
+    apply case (free_union Var) (der eq)
+    · grind
+    · grind
+  | app => grind
+  | tapp => grind [Sub.narrow]
+  | inl => grind [Ty.Wf.narrow]
+  | inr => grind [Ty.Wf.narrow]
+  | sub => grind [Sub.narrow]
 
 /-- Term substitution within a typing. -/
 lemma subst_tm (der : Typing (Γ ++ ⟨X, .ty σ⟩ :: Δ) t τ) (der_sub : Typing Δ s σ) :

From affa83ee9ab7b068f133364e5b5921bf6c944120 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 22 Mar 2026 09:34:41 -0400
Subject: [PATCH 14/14] ws

---
 .../LocallyNameless/Fsub/Typing.lean               | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
index c4fc11066..bd77e92fb 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Typing.lean
@@ -86,20 +86,20 @@ lemma weaken (der : Typing (Γ ++ Δ) t τ) (wf : (Γ ++ Θ ++ Δ).Wf) :
   | abs =>
     apply abs ((Γ ++ Θ ++ Δ).dom ∪ free_union Var)
     grind [Wf.weaken, Wf.of_env_ty]
-  | tabs => 
+  | tabs =>
     apply tabs ((Γ ++ Θ ++ Δ).dom ∪ free_union Var)
     grind [Wf.weaken, Wf.of_env_sub]
   | let' _ _ _ der =>
     apply let' ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq)
     grind
-  | case _ _ _ _ der => 
+  | case _ _ _ _ der =>
     apply case ((Γ ++ Θ ++ Δ).dom ∪ free_union Var) (der wf eq)
     · grind [Wf.weaken, Wf.of_env_ty]
     · grind [Wf.weaken, Wf.of_env_ty]
   | var => grind [<= sublist_dlookup]
   | app => grind
   | tapp => grind [Sub.weaken]
-  | inl => 
+  | inl =>
     -- TODO: break this and look at the way it's extending the context in the middle
     grind [Sub.weaken, Sub.refl]
   | inr => grind [Sub.weaken, Sub.refl]
@@ -118,16 +118,16 @@ lemma narrow (sub : Sub Δ δ δ') (der : Typing (Γ ++ ⟨X, Binding.sub δ'⟩
   | var =>
     -- TODO: split manually??
     grind [Env.Wf.narrow]
-  | abs  => 
+  | abs  =>
     apply abs (free_union Var)
     grind
-  | tabs => 
+  | tabs =>
     apply tabs (free_union Var)
     grind
-  | let' _ _ _ der => 
+  | let' _ _ _ der =>
     apply let' (free_union Var) (der eq)
     grind
-  | case _ _ _ _ der => 
+  | case _ _ _ _ der =>
     apply case (free_union Var) (der eq)
     · grind
     · grind