Exercise logic.propositional.dnf
Description
Proposition to DNF
Derivation
Final term is not finished
(T /\ ~(F || p)) <-> ~~(p /\ (q || q))
⇒ logic.propositional.notnot(T /\ ~(F || p)) <-> (p /\ (q || q))
⇒ logic.propositional.idempor(T /\ ~(F || p)) <-> (p /\ q)