adjust proofmode of_envs to rely less on persistently_emp_2

This is a first step towards #425 (being able to define persistence as False): the current definition of of_envs becomes False in that case, so this surely has to change. There are two equivalent formulations we could use:

⌜envs_wf' Γp Γs⌝ ∧ [∧] (env_map_pers Γp) ∧ [∗] Γs

or

⌜envs_wf' Γp Γs⌝ ∧ <affine> [∧] (env_map_pers Γp) ∗ [∗] Γs

Here, env_map_pers maps the persistence modality over the given environment.

I went with the first since having two ∧ seemed easier to deal with (and easier to parse) than mixing ∧ and ∗. Also it avoids a modality. However, some lemmas need to work with <affine> [∧] (env_map_pers Γp) since they involve separating conjunction. In the end I think both options are probably about equal in complexity, and the second option is slightly closer to what we have currently, but once I realized that I was already more than half-way done and re-proving all those environment lemmas did not seem worth it.