complete last part of env_elimination proof