diff --git a/CHANGELOG.md b/CHANGELOG.md
index a25e051f789583dafd45c18e8b4388e3a47b4f88..185bb7e8953b6a8bdeb8148a395c98973562fcdc 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -70,6 +70,8 @@ Coq 8.13 is no longer supported.
   timeless hypotheses when proving an invariant (without an update).
 * Make `uPred.unseal` tactic more robust by using types to unfold the right
   BI projections.
+* Turn `internal_eq_entails` into a bi-implication.
+* Add lemmas to relate internal/external non-expansiveness and contractiveness.
 
 **Changes in `heap_lang`:**
 
diff --git a/iris/base_logic/bi.v b/iris/base_logic/bi.v
index 954ab7b0d49419cd5a3eb8769be21fabbfec3354..698b949c72be88553c33f69a1527ffcc5070a4e7 100644
--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
@@ -216,7 +216,7 @@ Section restate.
   to express the more general case. This temporary proof rule will
   be replaced by the proper one eventually. *)
   Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
-    (∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2) → a1 ≡ a2 ⊢ b1 ≡ b2.
+    (a1 ≡ a2 ⊢ b1 ≡ b2) ↔ (∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2).
   Proof. exact: uPred_primitive.internal_eq_entails. Qed.
 
   Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
diff --git a/iris/base_logic/derived.v b/iris/base_logic/derived.v
index 16e37a82a08884d689c6d8f0acdc65f1237d084e..e0a03c895110069683b681f6fe4232bad1873f20 100644
--- a/iris/base_logic/derived.v
+++ b/iris/base_logic/derived.v
@@ -84,6 +84,36 @@ Section derived.
     MonoidHomomorphism op uPred_sep (≡) (@uPred_ownM M).
   Proof. split; [split|]; try apply _; [apply ownM_op | apply ownM_unit']. Qed.
 
+  (** Derive [NonExpansive]/[Contractive] from an internal statement *)
+  Lemma ne_internal_eq {A B : ofe} (f : A → B) :
+    NonExpansive f ↔ ∀ x1 x2, x1 ≡ x2 ⊢ f x1 ≡ f x2.
+  Proof.
+    split; [apply f_equivI|].
+    intros Hf n x1 x2. by eapply internal_eq_entails.
+  Qed.
+
+  Lemma ne_2_internal_eq {A B C : ofe} (f : A → B → C) :
+    NonExpansive2 f ↔ ∀ x1 x2 y1 y2, x1 ≡ x2 ∧ y1 ≡ y2 ⊢ f x1 y1 ≡ f x2 y2.
+  Proof.
+    split.
+    - intros Hf x1 x2 y1 y2.
+      change ((x1,y1).1 ≡ (x2,y2).1 ∧ (x1,y1).2 ≡ (x2,y2).2
+        ⊢ uncurry f (x1,y1) ≡ uncurry f (x2,y2)).
+      rewrite -prod_equivI. apply ne_internal_eq. solve_proper.
+    - intros Hf n x1 x2 Hx y1 y2 Hy.
+      change (uncurry f (x1,y1) ≡{n}≡ uncurry f (x2,y2)).
+      apply ne_internal_eq; [|done].
+      intros [??] [??]. rewrite prod_equivI. apply Hf.
+  Qed.
+
+  Lemma contractive_internal_eq {A B : ofe} (f : A → B) :
+    Contractive f ↔ ∀ x1 x2, ▷ (x1 ≡ x2) ⊢ f x1 ≡ f x2.
+  Proof.
+    split; [apply f_equivI_contractive|].
+    intros Hf n x1 x2 Hx. specialize (Hf x1 x2).
+    rewrite -later_equivI internal_eq_entails in Hf. apply Hf. by f_contractive.
+  Qed.
+
   (** Soundness statement for our modalities: facts derived under modalities in
   the empty context also without the modalities.
   For basic updates, soundness only holds for plain propositions. *)
diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v
index a1a1bb2378fad8583936480d1e2ba1855d0c72e5..2a7c443a53ac8ec33ef68ccb9cb23147fe3d4dea 100644
--- a/iris/base_logic/upred.v
+++ b/iris/base_logic/upred.v
@@ -810,8 +810,12 @@ Section primitive.
   to express the more general case. This temporary proof rule will
   be replaced by the proper one eventually. *)
   Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
-    (∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2) → a1 ≡ a2 ⊢ b1 ≡ b2.
-  Proof. unseal=>Hsi. split=>n x ?. apply Hsi. Qed.
+    (a1 ≡ a2 ⊢ b1 ≡ b2) ↔ (∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2).
+  Proof.
+    split.
+    - unseal=> -[Hsi] n. apply (Hsi _ ε), ucmra_unit_validN.
+    - unseal=> Hsi. split=>n x ?. apply Hsi.
+  Qed.
 
   (** Basic update modality *)
   Lemma bupd_intro P : P ⊢ |==> P.