EQ_BOOL_CONJ
⊢ (∀x y. ¬x ∨ (x ⇎ y) ∨ y) ∧ (∀x y. x ∨ (x ⇔ y) ∨ y) ∧ ∀x y. ¬x ∨ (x ⇔ y) ∨ ¬y
EQ_COMB
⊢ ∀f g x y. f ≠ g ∨ x ≠ y ∨ f x = g y
EQ_SYMTRANS
⊢ ∀x y z. x ≠ y ∨ x ≠ z ∨ y = z