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