From e424943560cb21518bdb9dbfd988fd3c7d9ed4f9 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Mon, 22 Jun 2026 14:31:10 -0400
Subject: [PATCH] chore: try fixing the Subtype.weaken proof

---
 .../LocallyNameless/Fsub/Subtype.lean         | 20 +++++++++++++------
 1 file changed, 14 insertions(+), 6 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean
index 7cdb72133..308fbe389 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Fsub/Subtype.lean
@@ -67,15 +67,23 @@ lemma refl (wf_Γ : Γ.Wf) (wf_σ : σ.Wf Γ) : Sub Γ σ σ := by
 /-- Weakening of subtypes. -/
 lemma weaken (sub : Sub (Γ ++ Θ) σ σ') (wf : (Γ ++ Δ ++ Θ).Wf) : Sub (Γ ++ Δ ++ Θ) σ σ' := by
   generalize eq : Γ ++ Θ = ΓΘ at sub
-  induction sub generalizing Γ
-  case all =>
+  induction sub generalizing Γ with
+  | trans_tvar => grind [Ty.Wf.weaken, <= sublist_dlookup]
+  | all _ _ _ ih ih₂ =>
+    subst eq
+    apply all (free_union [Context.dom] Var) (ih wf rfl)
+    grind
+  | top _ σ_wf =>
     subst eq
-    apply all (free_union [Context.dom] Var) <;> grind
-  all_goals grind [Ty.Wf.weaken, <= sublist_dlookup]
+    exact .top wf (weaken σ_wf wf.to_ok)
+  | refl_tvar _ fvar_wf =>
+    subst eq
+    exact Sub.refl_tvar wf (weaken fvar_wf wf.to_ok)
+  | _ => grind
 
 lemma weaken_head (sub : Sub Δ σ σ') (wf : (Γ ++ Δ).Wf) : Sub (Γ ++ Δ) σ σ' := by
-  have eq : Γ ++ Δ = [] ++ Γ ++ Δ := by grind
-  grind [weaken]
+  rw [← List.nil_append Γ]
+  exact weaken sub wf
 
 lemma narrow_aux
     (trans : ∀ Γ σ τ, Sub Γ σ δ → Sub Γ δ τ → Sub Γ σ τ)