diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index d743539a62c1e7b8833e8c1e86c354fbc58a010b..68c57a3f3cd01e38e9b5fbe14e57ff339e3e6367 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -604,6 +604,9 @@ Infix "â—Ž" := ccompose (at level 40, left associativity).
 Global Instance ccompose_ne {A B C} :
   NonExpansive2 (@ccompose A B C).
 Proof. intros n ?? Hf g1 g2 Hg x. rewrite /= (Hg x) (Hf (g2 x)) //. Qed.
+Global Instance ccompose_proper {A B C} :
+  Proper ((≡) ==> (≡) ==> (≡)) (@ccompose A B C).
+Proof. apply ne_proper_2; apply _. Qed.
 
 (* Function space maps *)
 Definition ofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B')