From 33f4b1ba6c53235aea0ea164721372d741ac5f2a 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 a830d898f..1fb91ecae 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. -/ @[scoped grind →]