diff --git a/theories/channel/proto_channel.v b/theories/channel/proto_channel.v
index b8e22453c00c059da2fba5bf77e0f95b12cc1ba6..6ba63659253b0267bbf65d306dd99a8f3171b678 100644
--- a/theories/channel/proto_channel.v
+++ b/theories/channel/proto_channel.v
@@ -216,6 +216,7 @@ Proof. solve_contractive. Qed.
 Definition iProto_le `{invG Σ} (p1 p2 : iProto Σ) : iProp Σ :=
   fixpoint iProto_le_aux p1 p2.
 Arguments iProto_le {_ _} _%proto _%proto.
+Instance: Params (@iProto_le) 2 := {}.
 
 Fixpoint proto_interp {Σ} (vs : list val) (p1 p2 : iProto Σ) : iProp Σ :=
   match vs with