Added missing variable to fix CI failure

theories/channel/proto.v

@@ -359,12 +359,14 @@ Section proto.
   Global Instance iMsg_car_proper :
     Proper (iMsg_equiv ==> (=) ==> (≡) ==> (≡)) (iMsg_car (Σ:=Σ) (V:=V)).
   Proof.
-    iIntros (m1 m2 meq v1 v2 veq p1 p2 peq). rewrite meq. by do 2 f_equiv=> //.
+    intros m1 m2 meq v1 v2 veq p1 p2 peq. rewrite meq.
+    f_equiv; [ by f_equiv | done ].
   Qed.
-  Global Instance iMsg_car_ne :
+  Global Instance iMsg_car_ne n :
     Proper (iMsg_dist n ==> (=) ==> (dist n) ==> (dist n)) (iMsg_car (Σ:=Σ) (V:=V)).
   Proof.
-    iIntros (n m1 m2 meq v1 v2 veq p1 p2 peq). rewrite meq. by do 2 f_equiv=> //.
+    intros m1 m2 meq v1 v2 veq p1 p2 peq. rewrite meq.
+    f_equiv; [ by f_equiv | done ].
   Qed.
 
   Global Instance iMsg_contractive v n :