simp only [Formula.IsTautoPrime]
P Q : Formula
⊢ (((P.iff_ Q).imp_ ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_
        (((P.imp_ Q).imp_ (Q.imp_ P).not_).not_.imp_ (P.iff_ Q)).not_).not_.IsTautoPrime
P Q : Formula
⊢ ∀ (V : VarBoolAssignment),
    evalPrime V
      (((P.iff_ Q).imp_ ((P.imp_ Q).imp_ (Q.imp_ P).not_).not_).imp_
          (((P.imp_ Q).imp_ (Q.imp_ P).not_).not_.imp_ (P.iff_ Q)).not_).not_