From efdbf7685e972d21962d396525659cd772c1f2da Mon Sep 17 00:00:00 2001 From: lengyijun Date: Fri, 18 Sep 2026 08:38:40 +0800 Subject: [PATCH] refactor: correct para_open_out variable orientation --- .../LocallyNameless/Untyped/FullBetaConfluence.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean index 3a9a2d19b..e95ef53ab 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaConfluence.lean @@ -132,8 +132,8 @@ lemma para_open_close (x y z) (para : M ⭢ₚ M') : M⟦z ↜ x⟧⟦z ↝ fvar by grind /-- Parallel substitution respects fresh opening. -/ -lemma para_open_out (L : Finset Var) (mem : ∀ x, x ∉ L → (M ^ fvar x) ⭢ₚ N ^ fvar x) - (para : M' ⭢ₚ N') : (M ^ M') ⭢ₚ (N ^ N') := by +lemma para_open_out (L : Finset Var) (mem : ∀ x, x ∉ L → (M ^ fvar x) ⭢ₚ M' ^ fvar x) + (para : N ⭢ₚ N') : (M ^ N) ⭢ₚ (M' ^ N') := by grind [fresh_exists <| free_union [fv] Var] -- TODO: the Takahashi translation would be a much nicer and shorter proof, but I had difficultly