From e02ad2dcc0f93107c18f8316b386b92b45548e97 Mon Sep 17 00:00:00 2001 From: Hannes Schulze Date: Sun, 30 Nov 2025 22:20:35 +0100 Subject: update lean --- Nominal/LambdaCalculus/Preterms.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Nominal/LambdaCalculus/Preterms.lean') diff --git a/Nominal/LambdaCalculus/Preterms.lean b/Nominal/LambdaCalculus/Preterms.lean index 74f7397..c133343 100644 --- a/Nominal/LambdaCalculus/Preterms.lean +++ b/Nominal/LambdaCalculus/Preterms.lean @@ -114,7 +114,7 @@ instance : NominalSet Var Preterm where simp only [PermSet.fix', smul_abs, Preterm.abs.injEq, Set.mem_setOf_eq] simp only [PermSet.fix, vars, Set.singleton_union, Set.mem_insert_iff, forall_eq_or_imp, Set.mem_setOf_eq] at hπ exact ⟨hπ.left, a_ih.left hπ.right⟩ - · simp [vars, Set.Finite.insert, a_ih] + · simp [vars, a_ih] · constructor · intro π hπ simp only [PermSet.fix', smul_app, Preterm.app.injEq, Set.mem_setOf_eq] -- cgit v1.3.1