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