diff --git a/modures/agree.v b/modures/agree.v
index 173c81977e039d9d1aa3e38623e0275999709309..212be59d339a148b11c1dc3c4f0392cec6fa5bc5 100644
--- a/modures/agree.v
+++ b/modures/agree.v
@@ -133,6 +133,8 @@ Proof. intros x1 x2 Hx; split; naive_solver eauto using @dist_le. Qed.
 Global Instance to_agree_proper : Proper ((≡) ==> (≡)) to_agree := ne_proper _.
 Global Instance to_agree_inj n : Injective (dist n) (dist n) (to_agree).
 Proof. by intros x y [_ Hxy]; apply Hxy. Qed.
+Lemma to_agree_car n (x : agree A) : ✓{n} x → to_agree (x n) ={n}= x.
+Proof. intros [??]; split; naive_solver eauto using agree_valid_le. Qed.
 End agree.
 
 Arguments agreeC : clear implicits.