simp only [isFreeIn]
case h1.h1.h2
P Q : Formula
v : VarName
⊢ ¬isFreeIn v (forall_ v P) ∧ ¬isFreeIn v (forall_ v ((P.imp_ Q).and_ (Q.imp_ P)))
case h1.h1.h2
P Q : Formula
v : VarName
⊢ ¬(¬True ∧ isFreeIn v P) ∧ ¬(¬True ∧ ((isFreeIn v P ∨ isFreeIn v Q) ∨ isFreeIn v Q ∨ isFreeIn v P))