tauto
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)))
no goals