Search
a ∨ b, b ⇒ (¬ c ∨ e), a ⇒ (¬c ∨ d) ⊢ c ⇒ (e ∨ d).
⊢ ((a ⇒ b) ⇒ a) ⇒ a.
∀x(∃y(M(x,y) ∨ M(y,x)) ⇒ M(x,x)), ∃x∃yM(x,y) ⊢ ∃xM(x,x)