diff --git a/algebra/ofe.v b/algebra/ofe.v
index 7b08c03cc6be5dc18fa7ca1abfaace672fcf857b..8812dc5ff362859859a399eb9bf6fa27f0ec67a6 100644
--- a/algebra/ofe.v
+++ b/algebra/ofe.v
@@ -770,13 +770,6 @@ 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 81d2539970b170daa7918ca97b8a84609fb7cc07..7361ad14752e70666af09eaad19906a3e2a13897 100644
--- a/base_logic/derived.v
+++ b/base_logic/derived.v
@@ -290,10 +290,8 @@ Proof. apply (internal_eq_rewrite a b (λ b, b ≡ a)%I); auto. solve_proper. Qe
 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.
+  move: HΨ=> /contractiveI HΨ Heq ?.
+  apply (internal_eq_rewrite (Ψ a) (Ψ b) id _)=>//=. by rewrite -HΨ.
 Qed.
 
 Lemma pure_impl_forall φ P : (⌜φ⌝ → P) ⊣⊢ (∀ _ : φ, P).
diff --git a/base_logic/primitive.v b/base_logic/primitive.v
index 033d562e57a48ed670f9544dcfa678d34d3e4581..510424fe41e31b189ea69c2a09677a9608bb0a43 100644
--- a/base_logic/primitive.v
+++ b/base_logic/primitive.v
@@ -581,6 +581,16 @@ Lemma option_validI {A : cmraT} (mx : option A) :
   ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True end.
 Proof. unseal. by destruct mx. Qed.
 
+(* Contractive functions *)
+Lemma contractiveI {A B : ofeT} (f : A → B) :
+  Contractive f ↔ (∀ x y, ▷ (x ≡ y) ⊢ f x ≡ f y).
+Proof.
+  split; unseal; intros Hf.
+  - intros x y; split=> -[|n] z _ /=; eauto using contractive_0, contractive_S.
+  - intros [|i] x y Hxy; apply (uPred_in_entails _ _ (Hf x y) _ ∅);
+      simpl; eauto using ucmra_unit_validN.
+Qed.
+
 (* Functions *)
 Lemma cofe_funC_equivI {A B} (f g : A -c> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
 Proof. by unseal. Qed.