diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index de26c43e83cafe89f47559b88c6e051cc0f1ab5c..df45c6aafe8bc00333b0759d1d8d66cfe536d436 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -959,6 +959,10 @@ Proof. rewrite /urFunctorContractive; apply _. Qed.
 Definition cmra_transport {A B : cmraT} (H : A = B) (x : A) : B :=
   eq_rect A id x _ H.
 
+Lemma cmra_transport_trans {A B C : cmraT} (H1 : A = B) (H2 : B = C) x :
+  cmra_transport H2 (cmra_transport H1 x) = cmra_transport (eq_trans H1 H2) x.
+Proof. by destruct H2. Qed.
+
 Section cmra_transport.
   Context {A B : cmraT} (H : A = B).
   Notation T := (cmra_transport H).