diff --git a/_CoqProject b/_CoqProject
index 330aec8252d15ca5be2cdef987318cd0b9f9f047..2fcbc7e214252b670e0b86a2d9ed1526a033df56 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -16,9 +16,10 @@ theories/utils/cofe_solver_2.v
 theories/utils/switch.v
 theories/channel/proto_model.v
 theories/channel/proto.v
+theories/channel/channel.v
 theories/channel/multi_proto_model.v
 theories/channel/multi_proto.v
-theories/channel/channel.v
+theories/channel/multi_channel.v
 theories/channel/proofmode.v
 theories/examples/basics.v
 theories/examples/equivalence.v
diff --git a/theories/channel/multi_proto.v b/theories/channel/multi_proto.v
index 984b84c80d13b0eea0c3d0820bb39146f4db2168..05b31f71207fb8027a5b9f1400c1e129c2a699fb 100644
--- a/theories/channel/multi_proto.v
+++ b/theories/channel/multi_proto.v
@@ -707,7 +707,7 @@ Section proto.
     iProto_own γ i (<(Send j)> m1) -∗
     iProto_own γ j (<(Recv i)> m2) -∗
     iMsg_car m1 v (Next p1) ==∗
-    ▷ ∃ p2, iMsg_car m2 v (Next p2) ∗ ▷ iProto_ctx γ ∗
+    ▷ ∃ p2, iMsg_car m2 v (Next p2) ∗ iProto_ctx γ ∗
             iProto_own γ i p1 ∗ iProto_own γ j p2.
   Proof.
     iIntros "Hctx Hi Hj Hm".
@@ -718,7 +718,7 @@ Section proto.
       (p2) "[Hm2 Hconsistent]".
     iMod (iProto_own_auth_update _ _ _ _ p2 with "Hauth Hj") as "[Hauth Hj]".
     iMod (iProto_own_auth_update _ _ _ _ p1 with "Hauth Hi") as "[Hauth Hi]".
-    iIntros "!>!>". iExists p2. iFrame. iIntros "!>". iExists _. iFrame.
+    iIntros "!>!>". iExists p2. iFrame. iExists _. iFrame.
   Qed.
 
   (* (** The instances below make it possible to use the tactics [iIntros], *)