diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2482b3d14e3c91f32e1e6ed1f85b896dc86fbd95..67524c9949b468e53883e5d15d4a0ad5a2661e09 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -155,6 +155,10 @@ Coq 8.13 is no longer supported.
   [proofmode/base.v](iris/proofmode/base.v) for documentation on how
   to use these tactics to convert your own fixed arity tactics to an n-ary
   variant.
+* Improve the `IntoPure` instance for internal equality. Whenever possible,
+  `a ≡ b` will now be simplified to `a = b` upon introduction into the pure 
+  context. This will break but simplify some existing proofs: 
+  `iIntros (H%leibniz_equiv)` should be replaced by `iIntros (H)`. (by Ike Mulder)
 
 **Changes in `base_logic`:**
 
diff --git a/iris/proofmode/class_instances_internal_eq.v b/iris/proofmode/class_instances_internal_eq.v
index af546a0daf7e8e7c6a75da66daffe8d61dae0354..b44a78702792432e1c5bc2cf470bc710b754de9f 100644
--- a/iris/proofmode/class_instances_internal_eq.v
+++ b/iris/proofmode/class_instances_internal_eq.v
@@ -7,13 +7,32 @@ Section class_instances_internal_eq.
 Context `{!BiInternalEq PROP}.
 Implicit Types P Q R : PROP.
 
+(* When a user calls [iPureIntro] on [⊢ a ≡ b], the following instance turns
+  turns this into the pure goal [a ≡ b : Prop].
+  If [a, b : A] with [LeibnizEquiv A], another candidate would be [a = b]. While
+  this does not lead to information loss, [=] is harder to prove than [≡]. We thus
+  leave such simplifications to the user (e.g. they can call [fold_leibniz]). *)
 Global Instance from_pure_internal_eq {A : ofe} (a b : A) :
   @FromPure PROP false (a ≡ b) (a ≡ b).
 Proof. by rewrite /FromPure pure_internal_eq. Qed.
 
-Global Instance into_pure_eq {A : ofe} (a b : A) :
-  Discrete a → @IntoPure PROP (a ≡ b) (a ≡ b).
-Proof. intros. by rewrite /IntoPure discrete_eq. Qed.
+(* On the other hand, when a user calls [iIntros "%H"] on [⊢ (a ≡ b) -∗ P],
+  it is most convenient if [H] is as strong as possible---meaning, the user would
+  rather get [H : a = b] than [H : a ≡ b]. This is only possible if the
+  equivalence on [A] implies Leibniz equality (i.e., we have [LeibnizEquiv A]).
+  If the equivalence on [A] does not imply Leibniz equality, we cannot simplify
+  [a ≡ b] any further.
+  The following instance implements above logic, while avoiding a double search
+  for [Discrete a]. *)
+Global Instance into_pure_eq {A : ofe} (a b : A) (P : Prop) :
+  Discrete a →
+  TCOr (TCAnd (LeibnizEquiv A) (TCEq P (a = b)))
+       (TCEq P (a ≡ b)) →
+  @IntoPure PROP (a ≡ b) P.
+Proof.
+  move=> ? [[? ->]|->]; rewrite /IntoPure discrete_eq; last done.
+  by rewrite leibniz_equiv_iff.
+Qed.
 
 Global Instance from_modal_Next {A : ofe} (x y : A) :
   FromModal (PROP1:=PROP) (PROP2:=PROP) True (modality_laterN 1)
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 0dcc19295b472999fea4d68eb59f2dff93fc6a0b..e9f7005e0db6e44cce68360668dd5f0532003135 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1003,6 +1003,36 @@ Lemma test_iIntros_rewrite P (x1 x2 x3 x4 : nat) :
   x1 = x2 → (⌜ x2 = x3 ⌝ ∗ ⌜ x3 ≡ x4 ⌝ ∗ P) -∗ ⌜ x1 = x4 ⌝ ∗ P.
 Proof. iIntros (?) "(-> & -> & $)"; auto. Qed.
 
+Lemma test_iIntros_leibniz_equiv `{!BiInternalEq PROP} {A : ofe} (x y : A) :
+  Discrete x → LeibnizEquiv A →
+  x ≡ y ⊢@{PROP} ⌜x = y⌝.
+Proof.
+  intros ??.
+  iIntros (->). (* test that the [IntoPure] instance converts [≡] into [=] *)
+  done.
+Qed.
+
+Lemma test_iIntros_leibniz_equiv_prod `{!BiInternalEq PROP}
+    {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
+  Discrete a1 → Discrete b1 → LeibnizEquiv A → LeibnizEquiv B →
+  (a1, b1) ≡ (a2, b2) ⊢@{PROP} ⌜a1 = a2⌝.
+Proof.
+  intros ????.
+  iIntros ([-> _]%pair_eq).
+  (* another test that the [IntoPure] instance converts [≡] into [=], also under
+  combinators *)
+  done.
+Qed.
+
+Lemma test_iPureIntro_leibniz_equiv `{!BiInternalEq PROP}
+    {A : ofe} `{!LeibnizEquiv A} (x y : A) :
+  (x ≡ y) → ⊢@{PROP} x ≡ y.
+Proof.
+  intros Heq. iPureIntro.
+  (* test that the [FromPure] instance does _not_ convert [≡] into [=] *)
+  exact Heq.
+Qed.
+
 Lemma test_iDestruct_rewrite_not_consume P (x1 x2 : nat) :
   (P -∗ ⌜ x1 = x2 ⌝) →
   P -∗ ⌜ x1 = x2 ⌝ ∗ P.