diff --git a/theories/channel/proto_channel.v b/theories/channel/proto_channel.v
index 1731375564e1017ecb733697cdc1ffb49181626f..8786e1ed1094367ffefad82c3d66e32d2018e32f 100644
--- a/theories/channel/proto_channel.v
+++ b/theories/channel/proto_channel.v
@@ -212,6 +212,7 @@ Local Instance iProto_le_aux_contractive {Σ} : Contractive (@iProto_le_aux Σ).
 Proof. solve_contractive. Qed.
 Definition iProto_le {Σ} (p1 p2 : iProto Σ) : iPropO Σ :=
   fixpoint iProto_le_aux p1 p2.
+Arguments iProto_le {_} _%proto _%proto.
 
 Fixpoint proto_interp {Σ} (vs : list val) (p1 p2 : iProto Σ) : iProp Σ :=
   match vs with