`S is persistent` is not formally defined

Multiple rules write `S is persistent`, but the notion of a proposition being persistent is not defined.

In Iris proper we have:
```
  P is persistent
------------------
P |- \persistently P
```

This could also be used to mark the persistent propositions `True`, t =_\tau t'` and `{P} e {Q}`, which currently have separate
rules.