simp only [eval_not, eval_imp]
P Q : Formula
⊢ ∀ (V : VarBoolAssignment), evalPrime V ((P.not_.imp_ Q.not_).imp_ (Q.imp_ P))
P Q : Formula
⊢ ∀ (V : VarBoolAssignment), (¬evalPrime V P → ¬evalPrime V Q) → evalPrime V Q → evalPrime V P