remove ununsed definitions
remove unused lemma 'env_addition'