fix proof of basis_sem_env_SOME

just using abbreviations within the tactic proof, c.f. issue #6