From e023c6f8c22fc8a8596e402936e25c2169e4c4a2 Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Fri, 14 Aug 2026 19:04:02 +0800
Subject: [PATCH 1/2] BetaAt.step_fv

---
 .../LambdaCalculus/LocallyNameless/Untyped/BetaAt.lean | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/BetaAt.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/BetaAt.lean
index 4e1abca44..b0532132e 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/BetaAt.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/BetaAt.lean
@@ -172,6 +172,16 @@ lemma BetaAt.le_countRedexes (h : BetaAt i M N) : i ≤ countRedexes N := by
 
 variable [DecidableEq Var]
 
+lemma BetaAt.step_fv (h : BetaAt i M M') : M'.fv ⊆ M.fv := by
+  induction h with
+  | outer _ _ => grind [open_preserve_not_fvar]
+  | appL _ _ => grind
+  | appR _ _ => grind
+  | abs xs _ _ =>
+    have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
+    have := open_close x
+    grind [open_preserve_not_fvar 0 M M']
+
 /-- Renaming a free variable preserves the position of the contracted redex. -/
 lemma BetaAt.rename (h : BetaAt i M M') (x y : Var) :
     BetaAt i (M[x := fvar y]) (M'[x := fvar y]) := by

From 72a1e67ebf81c6f5424424748a732d0c1fcbac20 Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Fri, 14 Aug 2026 19:21:51 +0800
Subject: [PATCH 2/2] wip

---
 .../LocallyNameless/Untyped/BetaAt.lean       | 45 ++++++++++++++++++-
 .../Untyped/LeftmostReduction.lean            |  6 +++
 .../Untyped/StandardReduction.lean            |  2 +-
 3 files changed, 51 insertions(+), 2 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/BetaAt.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/BetaAt.lean
index b0532132e..2fe3b3c1b 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/BetaAt.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/BetaAt.lean
@@ -152,8 +152,24 @@ lemma BetaAt.to_step [DecidableEq Var] (h : BetaAt i M N) (lc : LC M) : M ⭢β
 
 variable [HasFresh Var]
 
+lemma BetaAt.le_countRedexes_l (h : BetaAt i M N) : i < countRedexes M := by
+  induction h with
+  | outer => grind
+  | appL step =>
+    split
+    · grind
+    · exact le_trans (by omega) (countRedexes_app_le _ _)
+  | appR =>
+    split
+    · rw [countRedexes_app_abs (by assumption)]
+      omega
+    · exact le_trans (by omega) (countRedexes_app_le _ _)
+  | abs xs =>
+    have := fresh_exists xs
+    grind [countRedexes_open_fvar]
+
 /-- The position of a contracted redex is at most the redex count of the result. -/
-lemma BetaAt.le_countRedexes (h : BetaAt i M N) : i ≤ countRedexes N := by
+lemma BetaAt.le_countRedexes_r (h : BetaAt i M N) : i ≤ countRedexes N := by
   induction h with
   | outer => exact Nat.zero_le _
   | appL step =>
@@ -228,6 +244,33 @@ lemma BetaAt.abs_close {x : Var} (h : BetaAt i M M') (lc : LC M) :
   have hr : BetaAt i (M[x := fvar z]) (M'[x := fvar z]) := h.rename x z
   grind
 
+lemma BetaAt.unique (hn : BetaAt i M N) (hp : BetaAt i M P) : N = P := by
+  induction hn generalizing P with
+  | outer _ _ =>
+      generalize hi : 0 = i at hp
+      cases hp <;> grind
+  | appL hn ih =>
+      generalize hi : ( _ +  if (IsAbs _) then 1 else 0) = i at hp
+      cases hp with
+      | outer => grind
+      | appL => grind
+      | appR hp =>
+          apply BetaAt.le_countRedexes_l at hn
+          omega
+  | appR hn ih =>
+      generalize hi : ( _ +  if (IsAbs _) then 1 else 0) = i at hp
+      cases hp with
+      | outer => grind
+      | appR => grind
+      | appL hp =>
+          apply BetaAt.le_countRedexes_l at hp
+          omega
+  | abs xs _ ih => cases hp with | abs xs hp =>
+      have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
+      specialize ih x (by grind) (hp x (by grind))
+      apply_fun (fun t => close t x) at ih
+      rw [<- open_close_var, <- open_close_var] at ih <;> grind
+
 end LambdaCalculus.LocallyNameless.Untyped.Term
 
 end Cslib
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
index e690a3375..e2f14e510 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/LeftmostReduction.lean
@@ -92,6 +92,12 @@ lemma Leftmost.of_cbn (h : M ↠ₙ N) : M ↠ℓ N := by
 
 variable [DecidableEq Var] [HasFresh Var]
 
+lemma Leftmost.steps_fv (steps : M ↠ℓ M') : M'.fv ⊆ M.fv := by
+  induction steps with
+  | refl => grind
+  | tail _ h _ => apply BetaAt.step_fv at h
+                  grind
+
 /-- Leftmost reduction preserves local closure. -/
 lemma Leftmost.steps_lc_r (h : M ↠ℓ M') (lc : LC M) : LC M' := by
   induction h with
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
index 96324ac57..31393620f 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/StandardReduction.lean
@@ -163,7 +163,7 @@ lemma StandardSeq.le_countRedexes_of_ne (h : StandardSeq n M N) (hne : M ≠ N)
     n ≤ countRedexes N := by
   cases h with
   | refl => contradiction
-  | tail _ step _ => exact step.le_countRedexes
+  | tail _ step _ => exact step.le_countRedexes_r
 
 omit [HasFresh Var] in
 /-- Reducing the operator of an application yields a standard sequence, with the final position