⊢ ∃x.A^{\overline{u}}  ⊢ ∀x.(A ⊃ B) ; \overline{∀E} ; ⊢ ([a/x]A) ⊃ B ⊢ [a/x]A^{\overline{w}} ; \overline{⊃ E} ; ⊢ B \overline{∃E^{a,w}} ⊢ B \overline{⊃ I^{u}} ⊢ (∃x.A) ⊃ B

1