simp only [eval_and, eval_not, eval_imp, eval_iff]
P Q : Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V ((P.and_ Q).iff_ (P.imp_ Q.not_).not_)
P Q : Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V P ∧ evalPrime V Q ↔ ¬(evalPrime V P → ¬evalPrime V Q)