Stale porting entries against Iris Rocq master

[github-actions]

Detected by the nightly stale-porting check.

Workflow run: https://github.com/leanprover-community/iris-lean/actions/runs/31569862090

Lean revision:                 ee0d298456e36a9f2e779ec87b82cba282e5ae3c
Checked against Rocq revision: fdc7d586883e968095b74536c0d1e80ca30c3b26

Stale aliases (1):
  bi.persistently_exist_1

Stale ignores (0):

[alvinylt]

This is relevant to the recent change to the BI interface regarding the commutativity between the existential quantifier and <pers>, which does not hold for temporal logic reasoning (as discussed in the Iris Workshop). This axiom is instead moved to a separate type class.

[markusdemedeiros]

Nice! So we should adapt our BI interface as well, then?

[alvinylt]

Sure, we can port it at some point. This will involve some slight changes to icases (i.e. iDestruct in Rocq).

[markusdemedeiros]

Sounds good. In the meantime we should just remove the alias to silence the bot.