diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 5b9f3533a9378e2942eecfbe13c68044f5ed5300..d394efad9b75671e9279e2bff9e59d58e033894c 100644
--- a/theories/channel/channel.v
+++ b/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.
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index fe123a17589254c4a4e4c67a6defc7dec4b78104..70a07dbf60755a21c00d6c93be457202f9f5bd9d 100644
--- a/theories/channel/proto.v
+++ b/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}.