simp
case h1.h3
P Q : Formula
v : VarName
⊢ ∀ H ∈ {(forall_ v (P.imp_ Q.not_).not_.not_).not_}, ¬isFreeIn v H
case h1.h3
P Q : Formula
v : VarName
⊢ ¬isFreeIn v (forall_ v (P.imp_ Q.not_).not_.not_).not_