EQ_NEG_F
⊢ ∀a. (¬a ⇔ F) ⇔ (a ⇔ T)
EQ_NEG_T
⊢ ∀a. (¬a ⇔ T) ⇔ (a ⇔ F)
STRONG_CONJ_lem
⊢ ∀a b. a ∧ (a ⇒ b) ⇒ a ∧ b