From deacf33709dd90e868890d0ab0b96e2df158ace5 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Mon, 23 Nov 2020 17:37:35 +0100
Subject: [PATCH] Added proper and nonexpansive classes for iMsg_car

---
 theories/channel/proto.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 24d02b1..9d1fb7b 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -356,6 +356,17 @@ Section proto.
   Proof. by rewrite internal_eq_sym iProto_message_end_equivI. Qed.
 
   (** ** Non-expansiveness of operators *)
+  Global Instance iMsg_car_proper :
+    Proper (iMsg_equiv ==> (=) ==> (≡) ==> (≡)) (iMsg_car (Σ:=Σ) (V:=V)).
+  Proof.
+    iIntros (m1 m2 meq v1 v2 veq p1 p2 peq). rewrite meq. by do 2 f_equiv=> //.
+  Qed.
+  Global Instance iMsg_car_ne :
+    Proper (iMsg_dist n ==> (=) ==> (dist n) ==> (dist n)) (iMsg_car (Σ:=Σ) (V:=V)).
+  Proof.
+    iIntros (n m1 m2 meq v1 v2 veq p1 p2 peq). rewrite meq. by do 2 f_equiv=> //.
+  Qed.
+
   Global Instance iMsg_contractive v n :
     Proper (dist n ==> dist_later n ==> dist n) (iMsg_base (Σ:=Σ) (V:=V) v).
   Proof. rewrite iMsg_base_eq=> P1 P2 HP p1 p2 Hp w q /=. solve_contractive. Qed.
-- 
GitLab