apply deduction_theorem
P Q : Formula
v : VarName
⊢ IsProof ((forall_ v ((P.imp_ Q).and_ (Q.imp_ P))).imp_ ((forall_ v Q).imp_ (forall_ v P)))
case h1
P Q : Formula
v : VarName
⊢ IsDeduct (∅ ∪ {forall_ v ((P.imp_ Q).and_ (Q.imp_ P))}) ((forall_ v Q).imp_ (forall_ v P))