diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 7c86fd444fc956ce69687275e6f47c3bac590653..1f47dcf15e308c48b3d5818a3c21622591c9e910 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -209,6 +209,9 @@ Proof. exact: uPred_primitive.discrete_fun_validI. Qed.
 Lemma pure_soundness φ : bi_emp_valid (PROP:=uPredI M) ⌜ φ ⌝ → φ.
 Proof. apply pure_soundness. Qed.
 
+Lemma internal_eq_soundness {A : ofeT} (x y : A) : (True ⊢ x ≡ y) → x ≡ y.
+Proof. apply internal_eq_soundness. Qed.
+
 Lemma later_soundness P : bi_emp_valid (▷ P) → bi_emp_valid P.
 Proof. apply later_soundness. Qed.
 (** See [derived.v] for a similar soundness result for basic updates. *)
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index b2bf5f05ce1a1370d2ed08bdd05ba57d072120e6..6d4df735c79f9720a229d974f30694c99aef22cb 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -800,9 +800,17 @@ Lemma discrete_fun_validI {A} {B : A → ucmraT} (g : discrete_fun B) : ✓ g 
 Proof. by unseal. Qed.
 
 (** Consistency/soundness statement *)
+(** The lemmas [pure_soundness] and [internal_eq_soundness] should become an
+instance of [siProp] soundness in the future. *)
 Lemma pure_soundness φ : (True ⊢ ⌜ φ ⌝) → φ.
 Proof. unseal=> -[H]. by apply (H 0 ε); eauto using ucmra_unit_validN. Qed.
 
+Lemma internal_eq_soundness {A : ofeT} (x y : A) : (True ⊢ x ≡ y) → x ≡ y.
+Proof.
+  unseal=> -[H]. apply equiv_dist=> n.
+  by apply (H n ε); eauto using ucmra_unit_validN.
+Qed.
+
 Lemma later_soundness P : (True ⊢ ▷ P) → (True ⊢ P).
 Proof.
   unseal=> -[HP]; split=> n x Hx _.