diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 9d1fb7b4417e3885f45e85068c2671dc1675112a..93341be68ce528dab3cf2f9828b777f51cfafd5e 100644
--- a/theories/channel/proto.v
+++ b/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 :