LK では、∀xA(x)->∃xA(x) が証明できるというのがミソ。
対象全体が空でないことが仮定されている。
等号つきだと ∃x(x=x) が証明できる。