diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index f0319c0ca16fc9af0872ed10d5f8dfc2ced1c8b4..63eeb95151bd13974a5ca41edf28e9eb3274150d 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -493,7 +493,8 @@ Section proto.
   Proof.
     rewrite iProto_message_eq iProto_dual_eq /iProto_dual_def /iProto_map_app.
     etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
-    apply: proto_elim_message=> a' m1 m2 Hm; f_equiv; solve_proper.
+    rewrite /iProto_message_def. rewrite ->proto_elim_message; [done|].
+    intros a' m1 m2 Hm; f_equiv; solve_proper.
   Qed.
   Lemma iMsg_dual_base v P p :
     iMsg_dual (MSG v {{ P }}; p) ≡ (MSG v {{ P }}; iProto_dual p)%msg.
@@ -529,7 +530,8 @@ Section proto.
   Proof.
     rewrite iProto_message_eq iProto_app_eq /iProto_app_def /iProto_map_app.
     etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
-    apply: proto_elim_message=> a' m1 m2 Hm. f_equiv; solve_proper.
+    rewrite /iProto_message_def. rewrite ->proto_elim_message; [done|].
+    intros a' m1 m2 Hm. f_equiv; solve_proper.
   Qed.
 
   Global Instance iProto_app_ne : NonExpansive2 (@iProto_app Σ V).
diff --git a/theories/channel/proto_model.v b/theories/channel/proto_model.v
index 2d5ddb43a323c01564672c8802332d502be69350..0a9bf8da6fa1efdead90428620c781afb6432854 100644
--- a/theories/channel/proto_model.v
+++ b/theories/channel/proto_model.v
@@ -224,7 +224,8 @@ Lemma proto_map_message {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'
   ≡ proto_message a (λ v, g ◎ m v ◎ laterO_map (proto_map g gn)).
 Proof.
   rewrite proto_map_unfold /proto_map_aux /=.
-  apply: proto_elim_message=> a' m1 m2 Hm; f_equiv; solve_proper.
+  rewrite ->proto_elim_message; [done|].
+  intros a' m1 m2 Hm. f_equiv; solve_proper.
 Qed.
 
 Lemma proto_map_ne {V}