iRewrite and internal equality on predicates
Consider the following example: (Ignore saved_prop_own, I only needed it to make Coq happy)
Lemma test {A} (P Q : A -c> iProp) a i φ :
saved_prop_own i φ ★ P ≡ Q ⊢ P a ≡ Q a.
Proof.
iIntros "[_ #E]".
Fail iRewrite "E".
Abort.It seems to me that iRewrite should succeed here. Is there a logical reason for it to fail? (As opposed to an engineering reason.)
(We are using commit 9c5a95d3 in case that matters.)