A constructive proof of Skolem theorem for constructive logic
Gilles Dowek, Benjamin Werner · arXiv (Cornell University) · 2023
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.