meson_eq_elim
⊢ (a ⇔ b) ⇒ b ∨ ¬a
meson_eq_thms
⊢ x = x ∧ (x ≠ y ∨ x ≠ z ∨ y = z)
meson_imp_conv
⊢ a ∨ b ⇔ ¬b ⇒ a
meson_imp_elim
⊢ a ⇒ b ⇔ ¬a ∨ b
meson_not_imp_p
⊢ ¬p ⇒ p ⇔ p
meson_p_imp_not_p
⊢ p ⇒ ¬p ⇔ ¬p