From c95790f1f677cad8e94e5c43495383704e4a6c7d Mon Sep 17 00:00:00 2001 From: lengyijun Date: Wed, 24 Jun 2026 16:04:30 +0800 Subject: [PATCH] refactor(LocallyNameless/Untyped): rename close_open => close_openRec - Rename the general version with explicit depth `k` into `close_openRec` - Introduce a new theorem for `k = 0` : `close_open` --- .../LambdaCalculus/LocallyNameless/Untyped/Properties.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean index 36c6c816d..bd329e28a 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Properties.lean @@ -151,9 +151,13 @@ lemma close_open_to_subst (m n : Term Var) (x : Var) (m_lc : LC m) (n_lc : LC n) (m ^* x) ^ n = m [x := n] := close_openRec_to_subst m n x 0 m_lc n_lc /-- Closing and opening are inverses. -/ -lemma close_open (x : Var) (t : Term Var) (k : ℕ) (t_lc : LC t) : t⟦k ↜ x⟧⟦k ↝ fvar x⟧ = t := by +lemma close_openRec (x : Var) (t : Term Var) (k : ℕ) (t_lc : LC t) : t⟦k ↜ x⟧⟦k ↝ fvar x⟧ = t := by grind [subst_refl] +/-- Closing and opening are inverses. -/ +lemma close_open (x : Var) (t : Term Var) (t_lc : LC t) : (t ^* x) ^ fvar x = t := + close_openRec x t 0 t_lc + end LambdaCalculus.LocallyNameless.Untyped.Term end Cslib