Exercise logic.propositional.dnf

Description
Proposition to DNF

Derivation

q || p || ~~(p -> q)

⇒ logic.propositional.notnot

q || p || (p -> q)

⇒ logic.propositional.defimpl

q || p || ~p || q

⇒ logic.propositional.complor

q || T || q

⇒ logic.propositional.truezeroor

q || T