started implementing proof of env_addition -- only some trivial cases are left