  A natural deduction system for intuitionistic predicate logic with
existential \ instantiation rule presented here uses Hilbert's $\e$-symbol. It
is conservative over intuitionistic predicate logic. We provide a completeness
proof for a suitable Kripke semantics, sketch an approach to a normalization
proof, survey related work and state some open problems. Our system extends
intuitionistic systems with $\e$-symbol due to A. Dragalin and Sh. Maehara.
