This is a first step towards #425 (being able to define persistence as
False): the current definition of
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
⌜envs_wf' Γp Γs⌝ ∧ <affine> [∧] (env_map_pers Γp) ∗ [∗] Γs
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.