From 9fb6751e0573407bce52cb38146b36ce1677f2f8 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@groupoid.moe>
Date: Thu, 27 May 2021 14:20:57 +0200
Subject: [PATCH] Add a `Proper` instance for ccompose.

---
 iris/algebra/ofe.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index d743539a6..68c57a3f3 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')
-- 
GitLab