simp only [def_and_]
case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    (((forall_ v ((P.imp_ Q).and_ (Q.imp_ P))).imp_
          (((forall_ v P).imp_ (forall_ v Q)).and_ ((forall_ v Q).imp_ (forall_ v P)))).imp_
      ((((forall_ v P).imp_ P).and_ (P.imp_ (forall_ v P))).imp_
        ((forall_ v ((P.imp_ Q).and_ (Q.imp_ P))).imp_ ((P.imp_ (forall_ v Q)).and_ ((forall_ v Q).imp_ P)))))
case a.a
P Q : Formula
v : VarName
h1 : ¬isFreeIn v P
⊢ IsDeduct ∅
    (((forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_
          (((forall_ v P).imp_ (forall_ v Q)).imp_ ((forall_ v Q).imp_ (forall_ v P)).not_).not_).imp_
      ((((forall_ v P).imp_ P).imp_ (P.imp_ (forall_ v P)).not_).not_.imp_
        ((forall_ v ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_
          ((P.imp_ (forall_ v Q)).imp_ ((forall_ v Q).imp_ P).not_).not_)))