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