It's a separate theorem. I'm not quite sure where I've seen it before, but https://www.cs.princeton.edu/courses/archive/fall03/cs528/handouts/Pure%20Versus%20Im

It's a separate theorem. I'm not quite sure where I've seen it before, but https://www.cs.princeton.edu/courses/archive/fall03/cs528/handouts/Pure%20Versus%20Impure%20LISP.pdf https://www.cs.princeton.edu/courses/archive/fall03/cs528/ha... seems to the right thing. Generally I've also heard it mentioned in the context of Okasaki's book about purely functional data structures.