diff --git a/theories/channel/proto_channel.v b/theories/channel/proto_channel.v
index 1a69f5d8bf44d5c16410246ba8ee39b930c6d2c2..ea3b97e63c19ef64a212fdd0b934fada89c57593 100644
--- a/theories/channel/proto_channel.v
+++ b/theories/channel/proto_channel.v
@@ -597,9 +597,9 @@ Section proto.
   Qed.
 
   Lemma proto_interp_recv v vs p1 pc :
-     proto_interp (v :: vs) p1 (proto_message Receive pc) -∗ ∃ p2,
-       pc v (proto_eq_next p2) ∗
-       â–· proto_interp vs p1 p2.
+    proto_interp (v :: vs) p1 (proto_message Receive pc) -∗ ∃ p2,
+      pc v (proto_eq_next p2) ∗
+      proto_interp vs p1 p2.
   Proof.
     simpl. iDestruct 1 as (pc' p2) "(Heq & Hc & Hp2)". iExists p2. iFrame "Hp2".
     iDestruct (@proto_message_equivI with "Heq") as "[_ Heq]".