prove tagenv_accumulates

not sure it's enough: we might need to know what the extra bit of the
tagenv actually is