Quantifiers

• How to Prove (∀x P(x) → A) → ∃x(P(x) → A)
  A classical proof uses cases on A and requires a nonempty domain; the statement is not generally valid in intuitionistic logic.