  If the sequent (Gamma entails forall x exists y A) is provable in first order
constructive natural deduction, then the theory (Gamma, forall x (f (x)/y)A),
where f is a new function symbol, is a conservative extension of Gamma.
