LEFT_ABSORB_DISJ
⊢ ∀a b. a ∨ b ⇔ a ∨ ¬a ∧ b
LEFT_DISJ_TAC_lem
⊢ ∀a b. a ∨ b ⇔ ¬b ⇒ a
RIGHT_ABSORB_DISJ
⊢ ∀a b. a ∨ b ⇔ a ∧ ¬b ∨ b
RIGHT_DISJ_TAC_lem
⊢ ∀a b. a ∨ b ⇔ ¬a ⇒ b