From f0652b93665a94b30d4d4a4969a1e7c5d5d80193 Mon Sep 17 00:00:00 2001
From: Malvin Gattinger <malvin@w4eg.de>
Date: Sun, 29 Oct 2023 16:51:56 +0000
Subject: [PATCH] adjust type of lengthAdd

---
 Bml/Setsimp.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Bml/Setsimp.lean b/Bml/Setsimp.lean
index 369a3ae..2285b81 100644
--- a/Bml/Setsimp.lean
+++ b/Bml/Setsimp.lean
@@ -19,10 +19,10 @@ theorem sdiff_singleton_is_erase {X : Finset Formula} {ϕ : Formula} : X \ {ϕ}
   aesop
 
 @[simp]
-theorem lengthAdd {X : Finset Formula} :
-    ∀ {ϕ} (h : ϕ ∉ X), lengthOfSet (insert ϕ X) = lengthOfSet X + lengthOfFormula ϕ :=
+theorem lengthAdd {X : Finset Formula} {ϕ} :
+    ϕ ∉ X → lengthOfSet (insert ϕ X) = lengthOfSet X + lengthOfFormula ϕ :=
   by
-  intro psi notin
+  intro notin
   unfold lengthOfSet
   rw [Finset.sum_insert notin]
   apply Nat.add_comm
@@ -50,7 +50,7 @@ theorem lengthRemove (X : Finset Formula) :
     constructor
     aesop
     tauto
-  rw [anotherClaim] at claim 
+  rw [anotherClaim] at claim
   aesop
 
 @[simp]