Module prop::or

Tactics for Logical OR.

Functions

assoc	(a ∨ b) ∨ c => a ∨ (b ∨ c)
commute	a ∨ b => b ∨ a.
distrib	(a ∧ b) ∨ (a ∧ c) => a ∧ (b ∨ c)
from_de_morgan	¬(a ∧ b) => (¬a ∨ ¬b).
to_de_morgan	(¬a ∨ ¬b) => ¬(a ∧ b).