iRewrite throws away non-persistent hypotheses
From iris.proofmode Require Import tactics.
Lemma foo `{!BiInternalEq PROP} (A : ofe) (x y : A) :
x ≡ y ⊢@{PROP} y ≡ x.
Proof.
iIntros "H". iRewrite "H". (* H is gone *)
Since internal equality is persistent, there is no need for this.