[∃x.A(x)]2 [A(z)]1 ----------------------------- (1) A(z) --------- ∀x.A(x) ----------------------------- (2) ∃x.A(x) → ∀x.A(x)