Proved contractiveness of iProto_own and iProto_mapsto

theories/channel/channel.v

@@ -110,6 +110,10 @@ Instance: Params (@iProto_mapsto) 4 := {}.
 Notation "c ↣ p" := (iProto_mapsto c p)
   (at level 20, format "c  ↣  p").
 
+Instance iProto_mapsto_contractive `{!heapG Σ, !chanG Σ} c :
+  Contractive (iProto_mapsto c).
+Proof. rewrite iProto_mapsto_eq. solve_contractive.
+
 Definition iProto_choice {Σ} (a : action) (P1 P2 : iProp Σ)
     (p1 p2 : iProto Σ) : iProto Σ :=
   (<a @ (b : bool)> MSG #b {{ if b then P1 else P2 }}; if b then p1 else p2)%proto.

theories/channel/proto.v

@@ -338,6 +338,10 @@ Definition iProto_own `{!protoG Σ V}
 Arguments iProto_own {_ _ _} _ _%proto.
 Instance: Params (@iProto_own) 3 := {}.
 
+Instance iProto_own_contractive `{protoG Σ V} γ s :
+  Contractive (iProto_own γ s).
+Proof. solve_contractive. Qed.
+
 (** * Proofs *)
 Section proto.
   Context `{!protoG Σ V}.