On $E$-theorems

There are [1] many methods to construct for every proof of a sentence $\exists x A$ in Heyting (intuitionistic) arithmetic $HA$ [2] a term $t_p$ such that $A[t_p]$ is true (in some sence). It turns out that majority of these methods are equivalent: correspondent terms $t_p$ are convertible into one and the same natural number. This is proved here for three methods: (I) complete cut-elimination in the infinite formulation of $HA$ [3]; (II) recursive realizability [2]; (III) partial cut-elimination along the lines of Gentsen's 2-nd consistency proof [5]. [6] or normalization [7], [8]. It is shown that the process of cut-elimination by method (I) leads only to computation of values of terms associated with a given proof by methods (II) and (III).