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