diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 8ba330065fdee81cd93da85026e4d44d369ff7f6..3f5dedbc6732a58b705c8557737c51db2f67f2e6 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -142,6 +142,14 @@ Proof.
   rewrite -Hx. apply pure_intro. done.
 Qed.
 
+(* IntoInternalEq *)
+Global Instance into_internal_eq_internal_eq {A : ofeT} (x y : A) :
+  @IntoInternalEq PROP A (x ≡ y) x y.
+Proof. by rewrite /IntoInternalEq. Qed.
+Global Instance into_internal_eq_persistently {A : ofeT} (x y : A) P :
+  IntoInternalEq P x y → IntoInternalEq (□ P) x y.
+Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
+
 (* IntoPersistent *)
 Global Instance into_persistent_persistently_trans p P Q :
   IntoPersistent true P Q → IntoPersistent p (□ P) Q | 0.
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 57aae7cd8239553e4781a86c9bf742dc2369c49b..4ae845a03077989f76c80610e84b80ec69c57001 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -54,6 +54,11 @@ Class FromPure {M} (P : uPred M) (φ : Prop) := from_pure : ⌜φ⌝ ⊢ P.
 Arguments from_pure {_} _ _ {_}.
 Hint Mode FromPure + ! - : typeclass_instances.
 
+Class IntoInternalEq {M} {A : ofeT} (P : uPred M) (x y : A) :=
+  into_internal_eq : P ⊢ x ≡ y.
+Arguments into_internal_eq {_ _} _ _ _ {_}.
+Hint Mode IntoInternalEq + - ! - - : typeclass_instances.
+
 Class IntoPersistent {M} (p : bool) (P Q : uPred M) :=
   into_persistent : □?p P ⊢ □ Q.
 Arguments into_persistent {_} _ _ _ {_}.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 138b5c473835d65cdb6d3355cb3e9ce53dcb905d..9ef1ff584575d9be58cae64f39aac44e7b1f4c21 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -768,7 +768,7 @@ Qed.
 Lemma tac_rewrite Δ i p Pxy d Q :
   envs_lookup i Δ = Some (p, Pxy) →
   ∀ {A : ofeT} (x y : A) (Φ : A → uPred M),
-    (Pxy ⊢ x ≡ y) →
+    IntoInternalEq Pxy x y →
     (Q ⊣⊢ Φ (if d is Left then y else x)) →
     NonExpansive Φ →
     (Δ ⊢ Φ (if d is Left then x else y)) → Δ ⊢ Q.
@@ -784,7 +784,7 @@ Lemma tac_rewrite_in Δ i p Pxy j q P d Q :
   envs_lookup i Δ = Some (p, Pxy) →
   envs_lookup j Δ = Some (q, P) →
   ∀ {A : ofeT} Δ' x y (Φ : A → uPred M),
-    (Pxy ⊢ x ≡ y) →
+    IntoInternalEq Pxy x y →
     (P ⊣⊢ Φ (if d is Left then y else x)) →
     NonExpansive Φ →
     envs_simple_replace j q (Esnoc Enil j (Φ (if d is Left then x else y))) Δ = Some Δ' →
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 64fa26512e424e15a8868c64a35028323c5ac4e2..fd39e7ff2aab4b6604df5703c321d6458686e47a 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1628,11 +1628,9 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
   iPoseProofCore lem as true true (fun Heq =>
     eapply (tac_rewrite _ Heq _ _ lr);
       [env_reflexivity || fail "iRewrite:" Heq "not found"
-      |let P := match goal with |- ?P ⊢ _ => P end in
-       (* use ssreflect apply: which is better at dealing with unification
-       involving canonical structures. This is useful for the COFE canonical
-       structure in uPred_eq that it may have to infer. *)
-       apply: reflexivity || fail "iRewrite:" P "not an equality"
+      |apply _ ||
+       let P := match goal with |- IntoInternalEq ?P _ _ ⊢ _ => P end in
+       fail "iRewrite:" P "not an equality"
       |iRewriteFindPred
       |intros ??? ->; reflexivity|lazy beta; iClear Heq]).
 
@@ -1644,8 +1642,8 @@ Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) "in" constr(H)
     eapply (tac_rewrite_in _ Heq _ _ H _ _ lr);
       [env_reflexivity || fail "iRewrite:" Heq "not found"
       |env_reflexivity || fail "iRewrite:" H "not found"
-      |apply: reflexivity ||
-       let P := match goal with |- ?P ⊢ _ => P end in
+      |apply _ ||
+       let P := match goal with |- IntoInternalEq ?P _ _ ⊢ _ => P end in
        fail "iRewrite:" P "not an equality"
       |iRewriteFindPred
       |intros ??? ->; reflexivity