From c227a28e0e6fabd1b14185b924bd9e0e3928a6d2 Mon Sep 17 00:00:00 2001 From: lengyijun Date: Sun, 26 Jul 2026 08:00:57 +0800 Subject: [PATCH] fix: Simplify FullEta.step_lc_r proof When there's just one or maybe two calls to grind, we can inline it --- .../LambdaCalculus/LocallyNameless/Untyped/FullEta.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean index 2231d2b08..d2e9c3046 100644 --- a/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean +++ b/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullEta.lean @@ -40,9 +40,7 @@ variable {M M' N N' : Term Var} /-- The right side of an η-reduction is locally closed. -/ @[scoped grind →] -lemma step_lc_r (step : M ⭢ηᶠ M') : LC M' := by - refine Xi.step_lc_r ?_ step - grind +lemma step_lc_r (step : M ⭢ηᶠ M') : LC M' := Xi.step_lc_r (by grind) step /-- The left side of an η-reduction is locally closed. -/ lemma step_lc_l [HasFresh Var] (step : M ⭢ηᶠ M') : LC M := by