add back termination proof for compile_envref

not sure why this became necessary again, or maybe it was always..
get replTheory to build

that's all of the compiler proofs building on refactor now