prove do_app_SOME_enveq

a likely useful lemma for the next evaluate_enveq case