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.)