Heytiag predicate calculus with $\varepsilon$-symbol

It is known that the introduction of $\varepsilon$-symbol with $\varepsilon$-axioms $A[t]\to A[\varepsilon x A]$ leads to non-conservative extension. For example $\exists x(\rceil P_x\to\rceil Pb\&\rceil Pa)$ becomes derivable. A conservative extension is obtained by treating $\varepsilon$-symbol like $\iota$-symbol: for every occurence $\varepsilon x A[x,\alpha_1\dots,\alpha_n]$ in a sequent from a deduction formula $\forall\alpha_1\dots\forall\alpha_n\exists x A$ should occur in the antecedent of this sequent. Cut-elimination is proved for the resulting system $HPC^{\varepsilon}$. It is pointed out that the proof could be extended to $HPC$ with decidable equality and to Heyting arithmetic with free function variables and the principle of choice:
$$ \Gamma\to\forall x\exists y A;\quad\forall x A_y[f(x)],\quad\Gamma\to C\vdash\Gamma\to C. $$

The extension to Heyting arithmetic with bound variables of higher types and corresponding choice principle requires new ideas.