some simplifications in env_elimination proof, complete admitted cases