From 4e3550bcfdbfdf7a74e16420353fa22b14c53e78 Mon Sep 17 00:00:00 2001
From: lengyijun <sjtu5140809011@gmail.com>
Date: Tue, 19 May 2026 18:51:03 +0800
Subject: [PATCH] feat: remove open_fresh_preserve_not_fvar

`open_preserve_not_fvar` is the stronger version of `open_fresh_preserve_not_fvar`
---
 .../LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean   | 2 +-
 .../LambdaCalculus/LocallyNameless/Untyped/FullEta.lean    | 2 +-
 .../LambdaCalculus/LocallyNameless/Untyped/Properties.lean | 7 +------
 3 files changed, 3 insertions(+), 8 deletions(-)

diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
index 1b90ff1e6..f9a5f00c8 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean
@@ -104,7 +104,7 @@ lemma step_not_fv (step : M ⭢βᶠ N) (hw : w ∉ M.fv) : w ∉ N.fv := by
   | abs =>
     have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
     have := open_close x
-    grind [close_preserve_not_fvar, open_fresh_preserve_not_fvar]
+    grind [close_preserve_not_fvar, open_preserve_not_fvar]
   | _ => grind
 
 /-- Abstracting then closing preserves a single reduction. -/
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean
index 9907b11a2..10d29d35e 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean
@@ -69,7 +69,7 @@ lemma step_not_fv (step : M ⭢ηᶠ M') (hw : w ∉ M.fv) : w ∉ M'.fv := by
   | abs =>
     have ⟨x, _⟩ := fresh_exists <| free_union [fv] Var
     have := open_close x
-    grind [close_preserve_not_fvar, open_fresh_preserve_not_fvar]
+    grind [close_preserve_not_fvar, open_preserve_not_fvar]
   | _ => grind
 
 /-- Substitution of a fresh variable preserves an η-reduction step. -/
diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean
index aedd0be0b..5bb9979a9 100644
--- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean
+++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean
@@ -55,11 +55,6 @@ lemma swap_open_fvar_close (k n : ℕ) (x y : Var) (m : Term Var) (neq₁ : k 
 lemma close_preserve_not_fvar {k x y} (m : Term Var) (nmem : x ∉ m.fv) : x ∉ (m⟦k ↜ y⟧).fv := by
   induction m generalizing k <;> grind
 
-/-- Opening to a fresh free variable preserves free variables. -/
-lemma open_fresh_preserve_not_fvar {k x y} (m : Term Var) (nmem : x ∉ m.fv) (neq : x ≠ y) :
-    x ∉ (m⟦k ↝ fvar y⟧).fv := by
-  induction m generalizing k <;> grind
-
 /-- Opening preserves free variables. -/
 lemma open_preserve_not_fvar {k x} (m n : Term Var) (nmem_m : x ∉ m.fv) (nmem_n : x ∉ n.fv) :
     x ∉ (m⟦k ↝ n⟧).fv := by
@@ -144,7 +139,7 @@ lemma open_close_to_subst (m : Term Var) (x y : Var) (k : ℕ) (m_lc : LC m) :
     grind [
       swap_open, =_ swap_open_fvar_close,
       open_close x' (t⟦k+1 ↜ x⟧⟦k+1 ↝ fvar y⟧) 0, open_close x' (t[x := fvar y]) 0,
-      open_fresh_preserve_not_fvar, close_preserve_not_fvar, subst_preserve_not_fvar]
+       open_preserve_not_fvar, close_preserve_not_fvar, subst_preserve_not_fvar]
   | _ => grind
 
 /-- Closing and opening are inverses. -/