diff --git a/algebra/ofe.v b/algebra/ofe.v
index 8812dc5ff362859859a399eb9bf6fa27f0ec67a6..7b08c03cc6be5dc18fa7ca1abfaace672fcf857b 100644
--- a/algebra/ofe.v
+++ b/algebra/ofe.v
@@ -770,6 +770,13 @@ Section later.
   Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed.
   Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A).
   Proof. by intros x y. Qed.
+
+  Lemma later_car_compose_ne {B : ofeT} (f : A → B) :
+    (Contractive f) → ∀ n, Proper (dist n ==> dist n) (f ∘ later_car).
+  Proof.
+    move=> Hcont n [x] [y] /= Hxy. apply Hcont. intros m Hmn.
+    destruct n; first by (exfalso; omega). eapply dist_le', Hxy. omega.
+  Qed.
 End later.
 
 Arguments laterC : clear implicits.
diff --git a/base_logic/derived.v b/base_logic/derived.v
index b85c482beaff97759242af42059d9b2949d22cd3..81d2539970b170daa7918ca97b8a84609fb7cc07 100644
--- a/base_logic/derived.v
+++ b/base_logic/derived.v
@@ -287,6 +287,14 @@ Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
 Proof. by intros ->. Qed.
 Lemma internal_eq_sym {A : ofeT} (a b : A) : a ≡ b ⊢ b ≡ a.
 Proof. apply (internal_eq_rewrite a b (λ b, b ≡ a)%I); auto. solve_proper. Qed.
+Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A → uPred M) P
+  {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
+Proof.
+  rewrite -later_equivI. intros Heq.
+  change ((P ⊢ (Ψ ∘ later_car) (Next a)) → P ⊢ (Ψ ∘ later_car) (Next b)).
+  apply internal_eq_rewrite; last done.
+  exact: later_car_compose_ne.
+Qed.
 
 Lemma pure_impl_forall φ P : (⌜φ⌝ → P) ⊣⊢ (∀ _ : φ, P).
 Proof.
diff --git a/base_logic/primitive.v b/base_logic/primitive.v
index ed8841b31135c054c3ad34ee2462393a1196f3f2..033d562e57a48ed670f9544dcfa678d34d3e4581 100644
--- a/base_logic/primitive.v
+++ b/base_logic/primitive.v
@@ -375,14 +375,6 @@ Proof.
   - by symmetry; apply Hab with x.
   - by apply Ha.
 Qed.
-Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A → uPred M) P
-  {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
-Proof.
-  unseal; intros Hab Ha; split=> n x ??. apply HΨ with n a; auto.
-  - destruct n; intros m ?; first omega. apply (dist_le n); last omega.
-    symmetry. by destruct Hab as [Hab]; eapply (Hab (S n)).
-  - by apply Ha.
-Qed.
 
 (* BI connectives *)
 Lemma sep_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q'.
@@ -565,7 +557,7 @@ Proof. by unseal. Qed.
 Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
 Proof. by unseal. Qed.
 
-(* Later *)
+(* Type-level Later *)
 Lemma later_equivI {A : ofeT} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y).
 Proof. by unseal. Qed.