simp only [eval_iff, eval_not, eval_imp]
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_
P Q : Formula
⊢ ∀ (V : VarBoolAssignment),
    ¬(((evalPrime V P ↔ evalPrime V Q) → ¬((evalPrime V P → evalPrime V Q) → ¬(evalPrime V Q → evalPrime V P))) →
        ¬(¬((evalPrime V P → evalPrime V Q) → ¬(evalPrime V Q → evalPrime V P)) → (evalPrime V P ↔ evalPrime V Q)))