There are many sources cite that simply typed lambda calculus extended with fixed-point combinator is Turing complete. For example, Does there exist a Turing complete typed lambda calculus? or the following quote from Boltzmann Samplers for Closed Simply-Typed Lambda Terms (2017).
Extended with a fix-point operator, simply-typed lambda terms can be used as the intermediate language for compiling Turing-complete functional languages.
However, I haven't found proof of this statement.
Could you please suggest where I could find the proof or the guideline of how to prove this statement? Thank you.