A constructive proof of Skolem theorem for constructive logic

Gilles Dowek, Benjamin Werner

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 functio…