diff --git a/theories/channel/proto_channel.v b/theories/channel/proto_channel.v
index ac212d5bd596230b1e48047b1fae96f27fe5a412..63f4468e0f7a7af9dd2d20712f85d469b91df7e0 100644
--- a/theories/channel/proto_channel.v
+++ b/theories/channel/proto_channel.v
@@ -92,7 +92,8 @@ Definition iProto_branch {Σ} (a : action) (p1 p2 : iProto Σ) : iProto Σ :=
   iProto_message a (tele_app (TT:=TeleS (λ _: bool, TeleO))
                              (λ b, (#b, True%I, if b then p1 else p2))).
 Typeclasses Opaque iProto_branch.
-Instance: Params (@iProto_branch) 1.
+Arguments iProto_branch {_} _ _%proto _%proto.
+Instance: Params (@iProto_branch) 2.
 Infix "<+>" := (iProto_branch Send) (at level 85) : proto_scope.
 Infix "<&>" := (iProto_branch Receive) (at level 85) : proto_scope.