simp only [def_and_]
case h1.h2.a.h2.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.and_ Q)} ∪ {P.and_ Q}) ((P.and_ Q).imp_ Q)
case h1.h2.a.h2.a
P Q : Formula
v : VarName
⊢ IsDeduct ({exists_ v (P.imp_ Q.not_).not_} ∪ {(P.imp_ Q.not_).not_}) ((P.imp_ Q.not_).not_.imp_ Q)