diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index e495bd19ebea3996dfb1a8822523f35220129768..542defa242dedafa214b77c731541a109a35964b 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -177,11 +177,11 @@ Section channel.
     iProto_le (iProto_branch a P1 P2 p1 p2) (iProto_branch a P1 P2 p1' p2').
   Proof.
     iIntros "H". rewrite /iProto_branch. destruct a.
-    - iApply iProto_le_send'; iIntros "!>" (b) "HP /=".
+    - iApply iProto_le_send; iIntros "!>" (b) "HP /=".
       iExists b; iSplit; [done|]. destruct b.
       + iDestruct "H" as "[H _]". by iApply "H".
       + iDestruct "H" as "[_ H]". by iApply "H".
-    - iApply iProto_le_recv'; iIntros "!>" (b) "HP /=".
+    - iApply iProto_le_recv; iIntros "!>" (b) "HP /=".
       iExists b; iSplit; [done|]. destruct b.
       + iDestruct "H" as "[H _]". by iApply "H".
       + iDestruct "H" as "[_ H]". by iApply "H".
diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index abdef69fe4a98fa5c95471bfc6872fe6102a7152..7652a629cd6785f5d9b416af2d89aa4cbd0a4991 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -134,14 +134,14 @@ Section classes.
     rewrite /ActionDualIf /ProtoContNormalize /ProtoNormalize=> -> H.
     destruct d; simpl.
     - rewrite iProto_dual_message iProto_app_message. destruct a1; simpl.
-      + iApply iProto_le_recv; iIntros (x) "/= Hpc". iExists x.
+      + iApply iProto_le_recv; iIntros "!>" (x) "/= Hpc". iExists x.
         destruct (H x) as (-> & -> & Hle). iSplit; [done|]. by iFrame "Hpc".
-      + iApply iProto_le_send; iIntros (x) "/= Hpc". iExists x.
+      + iApply iProto_le_send; iIntros "!>" (x) "/= Hpc". iExists x.
         destruct (H x) as (-> & -> & Hle). iSplit; [done|]. by iFrame "Hpc".
     - rewrite iProto_app_message. destruct a1; simpl.
-      + iApply iProto_le_send; iIntros (x) "/= Hpc". iExists x.
+      + iApply iProto_le_send; iIntros "!>" (x) "/= Hpc". iExists x.
         destruct (H x) as (-> & -> & Hle). iSplit; [done|]. by iFrame "Hpc".
-      + iApply iProto_le_recv; iIntros (x) "/= Hpc". iExists x.
+      + iApply iProto_le_recv; iIntros "!>" (x) "/= Hpc". iExists x.
         destruct (H x) as (-> & -> & Hle). iSplit; [done|]. by iFrame "Hpc".
   Qed.
 
@@ -164,7 +164,7 @@ Section classes.
     rewrite /ActionDualIf /ProtoContNormalize /ProtoNormalize.
     rewrite tforall_forall=> ? Hpc1 Hpc2. destruct d, a1; simplify_eq/=.
     - rewrite iProto_dual_message iProto_app_message /=.
-      iApply iProto_le_swap. iIntros (x1 x2) "/= Hpc1 Hpc2 !>".
+      iApply iProto_le_swap. iIntros "!>" (x1 x2) "/= Hpc1 Hpc2".
       move: (Hpc1 x1); rewrite {Hpc1} !tele_app_bind /=; intros (->&->&Hpc).
       move: (Hpc2 x2); rewrite {Hpc2} TCEq_eq; intros Hpc2.
       iExists TT2, TT1, (λ.. x2, (tele_app vP2 x2, tele_app (tele_app pc12 x1) x2)),
@@ -172,7 +172,7 @@ Section classes.
       rewrite /= !tele_app_bind /= -!Hpc2 /=. do 2 (iSplit; [done|]). iFrame.
       iSplitR; [done|]. iSplitR; [iApply iProto_le_refl|]. done.
     - rewrite iProto_app_message /=.
-      iApply iProto_le_swap. iIntros (x1 x2) "/= Hpc1 Hpc2 !>".
+      iApply iProto_le_swap. iIntros "!>" (x1 x2) "/= Hpc1 Hpc2".
       move: (Hpc1 x1); rewrite {Hpc1} !tele_app_bind /=; intros (->&->&Hpc).
       move: (Hpc2 x2); rewrite {Hpc2} TCEq_eq; intros Hpc2.
       iExists TT2, TT1, (λ.. x2, (tele_app vP2 x2, tele_app (tele_app pc12 x1) x2)),
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 64ebbedae910a3fc2ee9660b3512d12952a9edc5..ff41f7b1cef33024b22ac024aee8c1a78adbc1a3 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -58,10 +58,9 @@ Arguments iProto_end {_ _}.
 Program Definition iProto_message_def {Σ V} {TT : tele} (a : action)
     (pc : TT → V * iProp Σ * iProto Σ V) : iProto Σ V :=
   proto_message a (λ v, λne p', ∃ x : TT,
-    (** We need the later to make [iProto_message] contractive *)
     ⌜ v = (pc x).1.1 ⌝ ∗
-    ▷ (pc x).1.2 ∗
-    p' ≡ Next (pc x).2)%I.
+    (pc x).1.2 ∗
+    p' ≡ (pc x).2)%I.
 Next Obligation. solve_proper. Qed.
 Definition iProto_message_aux : seal (@iProto_message_def). by eexists. Qed.
 Definition iProto_message := iProto_message_aux.(unseal).
@@ -146,31 +145,29 @@ Notation "<?> 'MSG' v ; p" :=
 Notation "'END'" := iProto_end : proto_scope.
 
 (** * Operations *)
-Program Definition iProto_map_cont {Σ V}
-    (rec : iProto Σ V → iProto Σ V) (pc : laterO (iProto Σ V) -n> iPropO Σ) :
-    laterO (iProto Σ V) -n> iPropO Σ :=
-  λne p2, (∃ p1, pc (Next p1) ∗ p2 ≡ Next (rec p1))%I.
+Program Definition iProto_map_app_cont {Σ V}
+    (rec : iProto Σ V → iProto Σ V) (pc : iProto Σ V -n> iPropO Σ) :
+    iProto Σ V -n> iPropO Σ :=
+  λne p1', (∃ p1, pc p1 ∗ p1' ≡ rec p1)%I.
 Next Obligation. solve_proper. Qed.
 
 Program Definition iProto_map_app_aux {Σ V}
     (f : action → action) (p2 : iProto Σ V)
-    (rec : iProto Σ V -n> iProto Σ V) : iProto Σ V -n> iProto Σ V := λne p1,
-  match proto_unfold p1 return _ with
-  | None => p2
-  | Some (a, pc) => proto_message (f a) (iProto_map_cont rec ∘ pc)
-  end.
+    (rec : iProto Σ V -n> iProto Σ V) : iProto Σ V -n> iProto Σ V := λne p,
+  proto_elim p2 (λ a pc,
+    proto_message (f a) (iProto_map_app_cont rec ∘ pc)) p.
 Next Obligation.
-  intros Σ V f p2 rec n p1 p1'
-    [[??][??] [-> Hf]|]%(ofe_mor_ne _ _ proto_unfold); last done.
-  f_equiv=> v pc; rewrite /= /iProto_map_cont /=. by repeat f_equiv.
+  intros Σ V f p2 rec n p1 p1' Hp. apply proto_elim_ne=> // a pc1 pc2 Hpc.
+  apply proto_message_contractive; destruct n as [|n]=> // v p'; simpl in *.
+  by repeat f_equiv.
 Qed.
 
 Instance iProto_map_app_aux_contractive {Σ V} f (p2 : iProto Σ V) :
   Contractive (iProto_map_app_aux f p2).
 Proof.
-  intros n rec1 rec2 Hrec p1. simpl.
-  destruct (proto_unfold p1) as [[a c]|]; last done.
-  f_equiv=> v p' /=. by repeat (f_contractive || f_equiv).
+  intros n rec1 rec2 Hrec p1; simpl. apply proto_elim_ne=> // a pc1 pc2 Hpc.
+  apply proto_message_contractive; destruct n as [|n]=> // v p'; simpl in *.
+  by repeat f_equiv.
 Qed.
 
 Definition iProto_map_app {Σ V} (f : action → action)
@@ -179,7 +176,7 @@ Definition iProto_map_app {Σ V} (f : action → action)
 
 Definition iProto_app_def {Σ V} (p1 p2 : iProto Σ V) : iProto Σ V :=
   iProto_map_app id p2 p1.
-Definition iProto_app_aux : seal (@iProto_app_def). by eexists. Qed.
+Definition iProto_app_aux : seal (@iProto_app_def). Proof. by eexists. Qed.
 Definition iProto_app := iProto_app_aux.(unseal).
 Definition iProto_app_eq : @iProto_app = @iProto_app_def := iProto_app_aux.(seal_eq).
 Arguments iProto_app {_ _} _%proto _%proto.
@@ -188,7 +185,7 @@ Infix "<++>" := iProto_app (at level 60) : proto_scope.
 
 Definition iProto_dual_def {Σ V} (p : iProto Σ V) : iProto Σ V :=
   iProto_map_app action_dual proto_end p.
-Definition iProto_dual_aux : seal (@iProto_dual_def). by eexists. Qed.
+Definition iProto_dual_aux : seal (@iProto_dual_def). Proof. by eexists. Qed.
 Definition iProto_dual := iProto_dual_aux.(unseal).
 Definition iProto_dual_eq :
   @iProto_dual = @iProto_dual_def := iProto_dual_aux.(seal_eq).
@@ -226,20 +223,14 @@ Definition iProto_le_pre {Σ V}
     p1 ≡ proto_message a1 pc1 ∗
     p2 ≡ proto_message a2 pc2 ∗
     match a1, a2 with
-    | Recv, Recv =>
-       ∀ v p1', pc1 v (Next p1') -∗
-         ◇ ∃ p2', ▷ rec p1' p2' ∗ pc2 v (Next p2')
-    | Send, Send =>
-       ∀ v p2', pc2 v (Next p2') -∗
-         ◇ ∃ p1', ▷ rec p1' p2' ∗ pc1 v (Next p1')
-    | Recv, Send =>
-       ∀ v1 v2 p1' p2',
-         pc1 v1 (Next p1') -∗ pc2 v2 (Next p2') -∗
-         ◇ ∃ pc1' pc2' pt,
-           ▷ rec p1' (proto_message Send pc1') ∗
-           ▷ rec (proto_message Recv pc2') p2' ∗
-           pc1' v2 (Next pt) ∗
-           pc2' v1 (Next pt)
+    | Recv, Recv => ▷ ∀ v p1', pc1 v p1' -∗ ∃ p2', rec p1' p2' ∗ pc2 v p2'
+    | Send, Send => ▷ ∀ v p2', pc2 v p2' -∗ ∃ p1', rec p1' p2' ∗ pc1 v p1'
+    | Recv, Send => ▷ ∀ v1 v2 p1' p2',
+       pc1 v1 p1' -∗ pc2 v2 p2' -∗ ∃ pc1' pc2' pt,
+         rec p1' (proto_message Send pc1') ∗
+         rec (proto_message Recv pc2') p2' ∗
+         pc1' v2 pt ∗
+         pc2' v1 pt
     | Send, Recv => False
     end.
 Instance iProto_le_pre_ne {Σ V} (rec : iProto Σ V → iProto Σ V → iProp Σ) :
@@ -248,8 +239,8 @@ Proof. solve_proper. Qed.
 
 Program Definition iProto_le_pre' {Σ V}
     (rec : iProto Σ V -n> iProto Σ V -n> iPropO Σ) :
-    iProto Σ V -n> iProto Σ V -n> iPropO Σ :=
-  λne p1 p2, iProto_le_pre (λ p1' p2', rec p1' p2') p1 p2.
+    iProto Σ V -n> iProto Σ V -n> iPropO Σ := λne p1 p2,
+  iProto_le_pre (λ p1' p2', rec p1' p2') p1 p2.
 Solve Obligations with solve_proper.
 Local Instance iProto_le_pre_contractive {Σ V} : Contractive (@iProto_le_pre' Σ V).
 Proof.
@@ -273,12 +264,12 @@ Fixpoint iProto_interp_aux {Σ V} (n : nat)
      (∃ vl vsl' pc p2',
        ⌜ vsl = vl :: vsl' ⌝ ∗
        iProto_le (proto_message Recv pc) pr ∗
-       pc vl (Next p2') ∗
+       pc vl p2' ∗
        iProto_interp_aux n vsl' vsr pl p2') ∨
      (∃ vr vsr' pc p1',
        ⌜ vsr = vr :: vsr' ⌝ ∗
        iProto_le (proto_message Recv pc) pl ∗
-       pc vr (Next p1') ∗
+       pc vr p1' ∗
        iProto_interp_aux n vsl vsr' p1' pr)
   end.
 Definition iProto_interp {Σ V} (vsl vsr : list V) (pl pr : iProto Σ V) : iProp Σ :=
@@ -347,7 +338,7 @@ Section proto.
   Proof.
     rewrite !tforall_forall=> Hv HP Hp.
     rewrite iProto_message_eq /iProto_message_def.
-    f_equiv=> v f /=. apply bi.exist_ne=> x.
+    apply proto_message_contractive; destruct n as [|n]=> // v f /=.
     repeat (apply Hv || apply HP || apply Hp || f_contractive || f_equiv).
   Qed.
   Lemma iProto_message_ne {TT} a (pc1 pc2 : TT → V * iProp Σ * iProto Σ V) n :
@@ -383,23 +374,16 @@ Section proto.
   Lemma iProto_dual_end' : iProto_dual (Σ:=Σ) (V:=V) proto_end ≡ proto_end.
   Proof.
     rewrite iProto_dual_eq /iProto_dual_def /iProto_map_app.
-    etrans; [eapply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
-    pose proof (proto_unfold_fold (V:=V)
-      (PROP:=iPropO Σ) (PROPn:=iPropO Σ) None) as Hfold.
-    by destruct (proto_unfold (proto_fold None))
-      as [[??]|] eqn:E; rewrite E; inversion Hfold.
+    etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
+    by rewrite proto_elim_end.
   Qed.
   Lemma iProto_dual_message' a pc :
     iProto_dual (Σ:=Σ) (V:=V) (proto_message a pc)
-    ≡ proto_message (action_dual a) (iProto_map_cont iProto_dual ∘ pc).
+    ≡ proto_message (action_dual a) (iProto_map_app_cont iProto_dual ∘ pc).
   Proof.
-    rewrite iProto_dual_eq /iProto_dual_def /iProto_map_app /proto_message.
-    etrans; [eapply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
-    pose proof (proto_unfold_fold (V:=V) (PROP:=iPropO Σ)
-      (PROPn:=iPropO Σ) (Some (a,pc))) as Hfold.
-    destruct (proto_unfold (proto_fold (Some (a, pc))))
-      as [[??]|] eqn:E; inversion Hfold as [?? [Ha Hpc]|]; simplify_eq/=.
-    rewrite /proto_message. do 3 f_equiv; intros v p'; simpl. by repeat f_equiv.
+    rewrite iProto_dual_eq /iProto_dual_def /iProto_map_app.
+    etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
+    apply: proto_elim_message=> a' pc1 pc2 Hpc; f_equiv; solve_proper.
   Qed.
 
   Lemma iProto_dual_end : iProto_dual (Σ:=Σ) (V:=V) END ≡ END%proto.
@@ -412,7 +396,7 @@ Section proto.
     rewrite iProto_message_eq /iProto_message_def iProto_dual_message' /=.
     do 2 f_equiv; intros p'; simpl. iSplit.
     - iDestruct 1 as (pd) "[H Hp']". iDestruct "H" as (x ->) "[Hpc Hpd]".
-      iExists x. iSplit; [done|]; iFrame. iRewrite "Hp'". iNext. by iRewrite "Hpd".
+      iExists x. iSplit; [done|]; iFrame. iRewrite "Hp'". by iRewrite "Hpd".
     - iDestruct 1 as (x ->) "[Hpc Hpd]"; auto 10.
   Qed.
 
@@ -423,36 +407,27 @@ Section proto.
     { by rewrite !iProto_dual_end'. }
     rewrite !iProto_dual_message' involutive.
     iApply proto_message_equivI; iSplit; [done|]; iIntros (v p') "/=".
-    iApply prop_ext; iIntros "!>"; iSplit.
+    iIntros "!>"; iApply prop_ext; iIntros "!>"; iSplit.
     - iDestruct 1 as (pd) "[H Hp']". iRewrite "Hp'".
-      iDestruct "H" as (pdd) "[H #Hpd]".
-      iApply (bi.internal_eq_rewrite); [|done]; iModIntro.
-      iRewrite "Hpd". by iRewrite ("IH" $! pdd).
-    - iIntros "H". destruct (Next_uninj p') as [p'' Hp']. iExists (iProto_dual p'').
-      rewrite Hp'. iSplitL; [by auto|]. iNext. by iRewrite ("IH" $! p'').
+      iDestruct "H" as (pdd) "[H Hpd]". iRewrite "Hpd". by iRewrite ("IH" $! pdd).
+    - iIntros "H". iExists (iProto_dual p').
+      iSplitL; [by auto|]. by iRewrite ("IH" $! p').
   Qed.
 
   (** ** Append *)
   Lemma iProto_app_end' p : (proto_end <++> p)%proto ≡ p.
   Proof.
     rewrite iProto_app_eq /iProto_app_def /iProto_map_app.
-    etrans; [eapply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
-    pose proof (proto_unfold_fold (V:=V)
-      (PROP:=iPropO Σ) (PROPn:=iPropO Σ) None) as Hfold.
-    by destruct (proto_unfold (proto_fold None))
-      as [[??]|] eqn:E; rewrite E; inversion Hfold.
+    etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
+    by rewrite proto_elim_end.
   Qed.
   Lemma iProto_app_message' a pc p2 :
     (proto_message a pc <++> p2)%proto
-    ≡ proto_message a (iProto_map_cont (flip iProto_app p2) ∘ pc).
+    ≡ proto_message a (iProto_map_app_cont (flip iProto_app p2) ∘ pc).
   Proof.
-    rewrite iProto_app_eq /iProto_app_def /iProto_map_app /proto_message.
-    etrans; [eapply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
-    pose proof (proto_unfold_fold (V:=V) (PROP:=iPropO Σ)
-      (PROPn:=iPropO Σ) (Some (a,pc))) as Hfold.
-    destruct (proto_unfold (proto_fold (Some (a, pc))))
-      as [[??]|] eqn:E; inversion Hfold as [?? [Ha Hpc]|]; simplify_eq/=.
-    rewrite /proto_message. do 3 f_equiv; intros v p'; simpl. by repeat f_equiv.
+    rewrite iProto_app_eq /iProto_app_def /iProto_map_app.
+    etrans; [apply (fixpoint_unfold (iProto_map_app_aux _ _))|]; simpl.
+    apply: proto_elim_message => a' pc1 pc2 Hpc. f_equiv; solve_proper.
   Qed.
 
   Global Instance iProto_app_ne : NonExpansive2 (@iProto_app Σ V).
@@ -465,8 +440,9 @@ Section proto.
     revert p1'. induction (lt_wf n) as [n _ IH]; intros p1.
     destruct (proto_case p1) as [->|(a&pc&->)].
     { by rewrite !iProto_app_end'. }
-    rewrite !iProto_app_message'. f_equiv=> v p' /=. f_equiv=> p12.
-    do 2 f_equiv. f_contractive. apply IH; eauto using dist_le with lia.
+    rewrite !iProto_app_message'.
+    apply proto_message_contractive; destruct n as [|n]=> // v p' /=.
+    do 4 f_equiv. apply IH; eauto using dist_le with lia.
   Qed.
   Global Instance iProto_app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@iProto_app Σ V).
   Proof. apply (ne_proper_2 _). Qed.
@@ -478,7 +454,7 @@ Section proto.
     rewrite iProto_message_eq /iProto_message_def iProto_app_message' /=.
     f_equiv=> v ps /=. iSplit.
     - iDestruct 1 as (p1') "[H Hps]". iDestruct "H" as (x ->) "[Hpc #Hp1']".
-      iExists x. iSplit; [done|]. iFrame. iRewrite "Hps". iNext. by iRewrite "Hp1'".
+      iExists x. iSplit; [done|]. iFrame. iRewrite "Hps". by iRewrite "Hp1'".
     - iDestruct 1 as (x ->) "[Hpc Hps]". auto 10.
   Qed.
 
@@ -492,12 +468,9 @@ Section proto.
     { by rewrite iProto_app_end'. }
     rewrite iProto_app_message'.
     iApply proto_message_equivI; iSplit; [done|]; iIntros (v p') "/=".
-    iApply prop_ext; iIntros "!>". iSplit.
-    - iDestruct 1 as (p1') "[H Hp']". iRewrite "Hp'".
-      iApply (bi.internal_eq_rewrite); [|done]; iModIntro.
-      by iRewrite ("IH" $! p1').
-    - iIntros "H". destruct (Next_uninj p') as [p'' Hp']. iExists p''.
-      rewrite Hp'. iFrame "H". iNext. by iRewrite ("IH" $! p'').
+    iIntros "!>". iApply prop_ext; iIntros "!>". iSplit.
+    - iDestruct 1 as (p1') "[H Hp']". iRewrite "Hp'". by iRewrite ("IH" $! p1').
+    - iIntros "H". iExists p'. iFrame "H". by iRewrite ("IH" $! p').
   Qed.
   Global Instance iProto_app_assoc : Assoc (≡) (@iProto_app Σ V).
   Proof.
@@ -506,13 +479,13 @@ Section proto.
     { by rewrite !iProto_app_end'. }
     rewrite !iProto_app_message'.
     iApply proto_message_equivI; iSplit; [done|]; iIntros (v p123) "/=".
-    iApply prop_ext; iIntros "!>". iSplit.
+    iIntros "!>". iApply prop_ext; iIntros "!>". iSplit.
     - iDestruct 1 as (p1') "[H #Hp']".
       iExists (p1' <++> p2)%proto. iSplitL; [by auto|].
-      iRewrite "Hp'". iNext. iApply "IH".
+      iRewrite "Hp'". iApply "IH".
     - iDestruct 1 as (p12) "[H #Hp123]". iDestruct "H" as (p1') "[H #Hp12]".
       iExists p1'. iFrame "H". iRewrite "Hp123".
-      iNext. iRewrite "Hp12". by iRewrite ("IH" $! p1').
+      iRewrite "Hp12". by iRewrite ("IH" $! p1').
   Qed.
 
   Lemma iProto_dual_app p1 p2 :
@@ -523,13 +496,13 @@ Section proto.
     { by rewrite iProto_dual_end' !iProto_app_end'. }
     rewrite iProto_dual_message' !iProto_app_message' iProto_dual_message' /=.
     iApply proto_message_equivI; iSplit; [done|]; iIntros (v p12) "/=".
-    iApply prop_ext; iIntros "!>". iSplit.
+    iIntros "!>"; iApply prop_ext; iIntros "!>". iSplit.
     - iDestruct 1 as (p12d) "[H #Hp12]". iDestruct "H" as (p1') "[H #Hp12d]".
       iExists (iProto_dual p1'). iSplitL; [by auto|].
-      iRewrite "Hp12". iNext. iRewrite "Hp12d". iApply "IH".
+      iRewrite "Hp12". iRewrite "Hp12d". iApply "IH".
     - iDestruct 1 as (p1') "[H #Hp12]". iDestruct "H" as (p1d) "[H #Hp1']".
       iExists (p1d <++> p2)%proto. iSplitL; [by auto|].
-      iRewrite "Hp12". iNext. iRewrite "Hp1'". by iRewrite ("IH" $! p1d p2).
+      iRewrite "Hp12". iRewrite "Hp1'". by iRewrite ("IH" $! p1d p2).
   Qed.
 
   (** ** Protocol entailment **)
@@ -546,9 +519,9 @@ Section proto.
     iLöb as "IH" forall (p). destruct (proto_case p) as [->|([]&pc&->)].
     - rewrite iProto_le_unfold. iLeft; by auto.
     - rewrite iProto_le_unfold. iRight. iExists _, _, _, _; do 2 (iSplit; [done|]).
-      iIntros (v p') "Hpc". iExists p'. iIntros "{$Hpc} !> !>". iApply "IH".
+      iIntros "!>" (v p') "Hpc". iExists p'. iFrame "Hpc". iApply "IH".
     - rewrite iProto_le_unfold. iRight. iExists _, _, _, _; do 2 (iSplit; [done|]).
-      iIntros (v p') "Hpc". iExists p'. iIntros "{$Hpc} !> !>". iApply "IH".
+      iIntros "!>" (v p') "Hpc". iExists p'. iFrame "Hpc". iApply "IH".
   Qed.
 
   Lemma iProto_le_end_inv p : iProto_le p proto_end -∗ p ≡ proto_end.
@@ -562,17 +535,13 @@ Section proto.
     iProto_le p1 (proto_message Send pc2) -∗ ∃ a1 pc1,
       p1 ≡ proto_message a1 pc1 ∗
       match a1 with
-      | Send =>
-         ∀ v p2', pc2 v (Next p2') -∗
-           ◇ ∃ p1', ▷ iProto_le p1' p2' ∗ pc1 v (Next p1')
-      | Recv =>
-         ∀ v1 v2 p1' p2',
-           pc1 v1 (Next p1') -∗ pc2 v2 (Next p2') -∗
-           ◇ ∃ pc1' pc2' pt,
-             ▷ iProto_le p1' (proto_message Send pc1') ∗
-             ▷ iProto_le (proto_message Recv pc2') p2' ∗
-             pc1' v2 (Next pt) ∗
-             pc2' v1 (Next pt)
+      | Send => ▷ ∀ v p2', pc2 v p2' -∗ ∃ p1', iProto_le p1' p2' ∗ pc1 v p1'
+      | Recv => ▷ ∀ v1 v2 p1' p2',
+         pc1 v1 p1' -∗ pc2 v2 p2' -∗ ∃ pc1' pc2' pt,
+           iProto_le p1' (proto_message Send pc1') ∗
+           iProto_le (proto_message Recv pc2') p2' ∗
+           pc1' v2 pt ∗
+           pc2' v1 pt
       end.
   Proof.
     rewrite iProto_le_unfold. iIntros "[[_ Heq]|H]".
@@ -580,23 +549,22 @@ Section proto.
     iDestruct "H" as (a1 a2 pc1 pc2') "(Hp1 & Hp2 & H)".
     iDestruct (proto_message_equivI with "Hp2") as (<-) "{Hp2} #Hpc".
     iExists _, _; iSplit; [done|]. destruct a1.
-    - iIntros (v p2'). by iRewrite ("Hpc" $! v (Next p2')).
-    - iIntros (v1 v2 p1' p2'). by iRewrite ("Hpc" $! v2 (Next p2')).
+    - iIntros "!>" (v p2'). by iRewrite ("Hpc" $! v p2').
+    - iIntros "!>" (v1 v2 p1' p2'). by iRewrite ("Hpc" $! v2 p2').
   Qed.
 
   Lemma iProto_le_recv_inv p1 pc2 :
     iProto_le p1 (proto_message Recv pc2) -∗ ∃ pc1,
       p1 ≡ proto_message Recv pc1 ∗
-      ∀ v p1', pc1 v (Next p1') -∗
-        ◇ ∃ p2', ▷ iProto_le p1' p2' ∗ pc2 v (Next p2').
+      ▷ ∀ v p1', pc1 v p1' -∗ ∃ p2', iProto_le p1' p2' ∗ pc2 v p2'.
   Proof.
     rewrite iProto_le_unfold. iIntros "[[_ Heq]|H]".
     { by iDestruct (proto_message_end_equivI with "Heq") as %[]. }
     iDestruct "H" as (a1 a2 pc1 pc2') "(Hp1 & Hp2 & H)".
     iDestruct (proto_message_equivI with "Hp2") as (<-) "{Hp2} #Hpc2".
     destruct a1; [done|]. iExists _; iSplit; [done|].
-    iIntros (v p1') "Hpc". iDestruct ("H" with "Hpc") as (p2') ">[Hle Hpc]".
-    iExists p2'. iFrame "Hle". by iRewrite ("Hpc2" $! v (Next p2')).
+    iIntros "!>" (v p1') "Hpc". iDestruct ("H" with "Hpc") as (p2') "[Hle Hpc]".
+    iExists p2'. iFrame "Hle". by iRewrite ("Hpc2" $! v p2').
   Qed.
 
   Lemma iProto_le_trans p1 p2 p3 :
@@ -610,82 +578,49 @@ Section proto.
       + iDestruct (iProto_le_send_inv with "H1") as (a1 pc1) "[Hp1 H1]".
         iRewrite "Hp1"; clear p1. rewrite iProto_le_unfold; iRight.
         iExists _, _, _, _; do 2 (iSplit; [done|]). destruct a1.
-        * iIntros (v p3') "Hpc".
-          iMod ("H2" with "Hpc") as (p2') "[Hle Hpc]".
-          iMod ("H1" with "Hpc") as (p1') "[Hle' Hpc]".
-          iExists p1'. iIntros "{$Hpc} !>". by iApply ("IH" with "Hle'").
-        * iIntros (v1 v3 p1' p3') "Hpc1 Hpc3".
-          iMod ("H2" with "Hpc3") as (p2') "[Hle Hpc2]".
-          iMod ("H1" with "Hpc1 Hpc2") as (pc1' pc2' pt) "(Hp1' & Hp2' & Hpc)".
-          iModIntro. iExists pc1', pc2', pt. iFrame "Hp1' Hpc".
-          by iApply ("IH" with "Hp2'").
+        * iIntros "!>" (v p3') "Hpc".
+          iDestruct ("H2" with "Hpc") as (p2') "[Hle Hpc]".
+          iDestruct ("H1" with "Hpc") as (p1') "[Hle' Hpc]".
+          iExists p1'. iFrame "Hpc". by iApply ("IH" with "Hle'").
+        * iIntros "!>" (v1 v3 p1' p3') "Hpc1 Hpc3".
+          iDestruct ("H2" with "Hpc3") as (p2') "[Hle Hpc2]".
+          iDestruct ("H1" with "Hpc1 Hpc2") as (pc1' pc2' pt) "(Hp1' & Hp2' & Hpc)".
+          iExists pc1', pc2', pt. iFrame "Hp1' Hpc". by iApply ("IH" with "Hp2'").
       + iDestruct (iProto_le_recv_inv with "H1") as (pc1) "[Hp1 H1]".
         iRewrite "Hp1"; clear p1. rewrite iProto_le_unfold; iRight.
         iExists _, _, _, _; do 2 (iSplit; [done|]); simpl.
-        iIntros (v1 v3 p1' p3') "Hpc1 Hpc3".
-        iMod ("H1" with "Hpc1") as (p2') "[Hle Hpc2]".
-        iMod ("H2" with "Hpc2 Hpc3") as (pc2' pc3' pt) "(Hp2' & Hp3' & Hpc)".
-        iModIntro. iExists pc2', pc3', pt. iFrame "Hp3' Hpc".
-        by iApply ("IH" with "Hle").
+        iIntros "!>" (v1 v3 p1' p3') "Hpc1 Hpc3".
+        iDestruct ("H1" with "Hpc1") as (p2') "[Hle Hpc2]".
+        iDestruct ("H2" with "Hpc2 Hpc3") as (pc2' pc3' pt) "(Hp2' & Hp3' & Hpc)".
+        iExists pc2', pc3', pt. iFrame "Hp3' Hpc". by iApply ("IH" with "Hle").
     - iDestruct (iProto_le_recv_inv with "H2") as (pc2) "[Hp2 H3]".
       iRewrite "Hp2" in "H1".
       iDestruct (iProto_le_recv_inv with "H1") as (pc1) "[Hp1 H2]".
       iRewrite "Hp1". rewrite iProto_le_unfold. iRight.
       iExists _, _, _, _; do 2 (iSplit; [done|]).
-      iIntros (v p1') "Hpc".
-      iMod ("H2" with "Hpc") as (p2') "[Hle Hpc]".
-      iMod ("H3" with "Hpc") as (p3') "[Hle' Hpc]".
-      iModIntro. iExists p3'. iIntros "{$Hpc} !>". by iApply ("IH" with "Hle").
+      iIntros "!>" (v p1') "Hpc".
+      iDestruct ("H2" with "Hpc") as (p2') "[Hle Hpc]".
+      iDestruct ("H3" with "Hpc") as (p3') "[Hle' Hpc]".
+      iExists p3'. iFrame "Hpc". by iApply ("IH" with "Hle").
   Qed.
 
   Lemma iProto_le_send {TT1 TT2} (pc1 : TT1 → V * iProp Σ * iProto Σ V)
       (pc2 : TT2 → V * iProp Σ * iProto Σ V) :
-    (∀.. x2 : TT2, ▷ (pc2 x2).1.2 -∗ ◇ ∃.. x1 : TT1,
-      ⌜(pc1 x1).1.1 = (pc2 x2).1.1⌝ ∗
-      ▷ (pc1 x1).1.2 ∗
-      ▷ iProto_le (pc1 x1).2 (pc2 x2).2) -∗
-    iProto_le (iProto_message Send pc1) (iProto_message Send pc2).
-  Proof.
-    iIntros "H". rewrite iProto_le_unfold iProto_message_eq.
-    iRight. iExists _, _, _, _; do 2 (iSplit; [done|]).
-    iIntros (v p2') "/=". iDestruct 1 as (x2 ->) "[Hpc #Heq]".
-    iMod ("H" with "Hpc") as (x1 ?) "[Hpc Hle]".
-    iModIntro. iExists (pc1 x1).2. iSplitL "Hle".
-    { iIntros "!>". by iRewrite "Heq". }
-    iExists x1. iSplit; [done|]. iSplit; [by iApply "Hpc"|done].
-  Qed.
-  (* The following derived rule is weaker, but the positions of the laters
-  make more sense intuitively and practically. *)
-  Lemma iProto_le_send' {TT1 TT2} (pc1 : TT1 → V * iProp Σ * iProto Σ V)
-      (pc2 : TT2 → V * iProp Σ * iProto Σ V) :
     ▷ (∀.. x2 : TT2, (pc2 x2).1.2 -∗ ∃.. x1 : TT1,
       ⌜(pc1 x1).1.1 = (pc2 x2).1.1⌝ ∗
       (pc1 x1).1.2 ∗
       iProto_le (pc1 x1).2 (pc2 x2).2) -∗
     iProto_le (iProto_message Send pc1) (iProto_message Send pc2).
-  Proof.
-    iIntros "H". iApply iProto_le_send. iIntros (x2) "Hpc".
-    rewrite bi_tforall_forall. iDestruct ("H" with "Hpc") as "H".
-    rewrite bi_texist_exist bi.later_exist_except_0.
-    iMod "H" as (x1) "(>% & Hpc & Hle)". iExists x1. by iFrame.
-  Qed.
-
-  Lemma iProto_le_recv {TT1 TT2} (pc1 : TT1 → V * iProp Σ * iProto Σ V)
-      (pc2 : TT2 → V * iProp Σ * iProto Σ V) :
-    (∀.. x1 : TT1, ▷ (pc1 x1).1.2 -∗ ◇ ∃.. x2 : TT2,
-      ⌜(pc1 x1).1.1 = (pc2 x2).1.1⌝ ∗
-      ▷ (pc2 x2).1.2 ∗
-      ▷ iProto_le (pc1 x1).2 (pc2 x2).2) -∗
-    iProto_le (iProto_message Recv pc1) (iProto_message Recv pc2).
   Proof.
     iIntros "H". rewrite iProto_le_unfold iProto_message_eq.
     iRight. iExists _, _, _, _; do 2 (iSplit; [done|]).
-    iIntros (v p1') "/=". iDestruct 1 as (x1 ->) "[Hpc #Heq]".
-    iMod ("H" with "Hpc") as (x2 ?) "[Hpc Hle]". iExists (pc2 x2).2. iSplitL "Hle".
-    { iIntros "!> !>". by iRewrite "Heq". }
-    iModIntro. iExists x2. iSplit; [done|]. iSplit; [by iApply "Hpc"|done].
+    iIntros "!>" (v p2') "/=". iDestruct 1 as (x2 ->) "[Hpc #Heq]".
+    iDestruct ("H" with "Hpc") as (x1 ?) "[Hpc Hle]".
+    iExists (pc1 x1).2. iSplitL "Hle"; [by iRewrite "Heq"|].
+    iExists x1. iSplit; [done|]. iSplit; [by iApply "Hpc"|done].
   Qed.
-  Lemma iProto_le_recv' {TT1 TT2} (pc1 : TT1 → V * iProp Σ * iProto Σ V)
+
+  Lemma iProto_le_recv {TT1 TT2} (pc1 : TT1 → V * iProp Σ * iProto Σ V)
       (pc2 : TT2 → V * iProp Σ * iProto Σ V) :
     ▷ (∀.. x1 : TT1, (pc1 x1).1.2 -∗ ∃.. x2 : TT2,
       ⌜(pc1 x1).1.1 = (pc2 x2).1.1⌝ ∗
@@ -693,38 +628,16 @@ Section proto.
       iProto_le (pc1 x1).2 (pc2 x2).2) -∗
     iProto_le (iProto_message Recv pc1) (iProto_message Recv pc2).
   Proof.
-    iIntros "H". iApply iProto_le_recv. iIntros (x2) "Hpc".
-    rewrite bi_tforall_forall. iDestruct ("H" with "Hpc") as "H".
-    rewrite bi_texist_exist bi.later_exist_except_0.
-    iMod "H" as (x1) "(>% & Hpc & Hle)". iExists x1. by iFrame.
+    iIntros "H". rewrite iProto_le_unfold iProto_message_eq.
+    iRight. iExists _, _, _, _; do 2 (iSplit; [done|]).
+    iIntros "!>" (v p1') "/=". iDestruct 1 as (x1 ->) "[Hpc #Heq]".
+    iDestruct ("H" with "Hpc") as (x2 ?) "[Hpc Hle]".
+    iExists (pc2 x2).2. iSplitL "Hle"; [by iRewrite "Heq"|].
+    iExists x2. iSplit; [done|]. iSplit; [by iApply "Hpc"|done].
   Qed.
 
   Lemma iProto_le_swap {TT1 TT2} (pc1 : TT1 → V * iProp Σ * iProto Σ V)
       (pc2 : TT2 → V * iProp Σ * iProto Σ V) :
-    (∀.. (x1 : TT1) (x2 : TT2),
-      ▷ (pc1 x1).1.2 -∗ ▷ (pc2 x2).1.2 -∗
-      ◇ ∃ {TT3 TT4} (pc3 : TT3 → V * iProp Σ * iProto Σ V)
-          (pc4 : TT4 → V * iProp Σ * iProto Σ V), ∃.. (x3 : TT3) (x4 : TT4),
-        ⌜(pc1 x1).1.1 = (pc4 x4).1.1⌝ ∗
-        ⌜(pc2 x2).1.1 = (pc3 x3).1.1⌝ ∗
-        ▷ iProto_le (pc1 x1).2 (iProto_message Send pc3) ∗
-        ▷ iProto_le (iProto_message Recv pc4) (pc2 x2).2 ∗
-        ▷ (pc3 x3).1.2 ∗ ▷ (pc4 x4).1.2 ∗
-        ▷ ((pc3 x3).2 ≡ (pc4 x4).2)) -∗
-    iProto_le (iProto_message Recv pc1) (iProto_message Send pc2).
-  Proof.
-    iIntros "H". rewrite iProto_le_unfold iProto_message_eq.
-    iRight. iExists _, _, _, _; do 2 (iSplit; [done|]); simpl.
-    iIntros (v1 v2 p1 p2).
-    iDestruct 1 as (x1 ->) "[Hpc1 #Heq1]"; iDestruct 1 as (x2 ->) "[Hpc2 #Heq2]".
-    iMod ("H" with "Hpc1 Hpc2")
-      as (TT3 TT4 pc3 pc4 x3 x4 ??) "(H1 & H2 & Hpc1 & Hpc2 & #H)".
-    iModIntro. iExists _, _, (pc3 x3).2. iSplitL "H1"; [iNext; by iRewrite "Heq1"|].
-    iSplitL "H2"; [iNext; by iRewrite "Heq2"|]. simpl.
-    iSplitL "Hpc1"; [by auto|]. iExists x4. rewrite !bi.later_equivI. auto.
-  Qed.
-  Lemma iProto_le_swap' {TT1 TT2} (pc1 : TT1 → V * iProp Σ * iProto Σ V)
-      (pc2 : TT2 → V * iProp Σ * iProto Σ V) :
     ▷ (∀.. (x1 : TT1) (x2 : TT2),
       (pc1 x1).1.2 -∗ (pc2 x2).1.2 -∗
       ∃ {TT3 TT4} (pc3 : TT3 → V * iProp Σ * iProto Σ V)
@@ -737,16 +650,14 @@ Section proto.
         ((pc3 x3).2 ≡ (pc4 x4).2)) -∗
     iProto_le (iProto_message Recv pc1) (iProto_message Send pc2).
   Proof.
-    iIntros "H". iApply iProto_le_swap. iIntros (x1 x2) "Hpc1 Hpc2".
-    repeat setoid_rewrite bi_tforall_forall. iDestruct ("H" with "Hpc1 Hpc2") as "H".
-    iMod (bi.later_exist_except_0 with "H") as (TT3) "H".
-    iMod (bi.later_exist_except_0 with "H") as (TT4) "H".
-    iMod (bi.later_exist_except_0 with "H") as (pc3) "H".
-    iMod (bi.later_exist_except_0 with "H") as (pc4) "H".
-    rewrite bi_texist_exist bi.later_exist_except_0. iMod "H" as (x3) "H".
-    rewrite bi_texist_exist bi.later_exist_except_0. iMod "H" as (x4) "H".
-    iDestruct "H" as "(>% & >% & H1 & H2 & Hpc1 & Hpc2 & #H)".
-    iExists TT3, TT4, pc3, pc4, x3, x4. iFrame. auto.
+    iIntros "H". rewrite iProto_le_unfold iProto_message_eq.
+    iRight. iExists _, _, _, _; do 2 (iSplit; [done|]); simpl.
+    iIntros "!>" (v1 v2 p1 p2).
+    iDestruct 1 as (x1 ->) "[Hpc1 #Heq1]"; iDestruct 1 as (x2 ->) "[Hpc2 #Heq2]".
+    iDestruct ("H" with "Hpc1 Hpc2")
+      as (TT3 TT4 pc3 pc4 x3 x4 ??) "(H1 & H2 & Hpc1 & Hpc2 & #H)".
+    iExists _, _, (pc3 x3).2. iSplitL "H1"; [by iRewrite "Heq1"|].
+    iSplitL "H2"; [by iRewrite "Heq2"|]. simpl. iSplitL "Hpc1"; eauto.
   Qed.
 
   Lemma iProto_le_swap_simple {TT1 TT2} (v1 : TT1 → V) (v2 : TT2 → V)
@@ -757,7 +668,7 @@ Section proto.
         (iProto_message Send (λ x2,
           (v2 x2, P2 x2, iProto_message Recv (λ x1, (v1 x1, P1 x1, p x1 x2))))).
   Proof.
-    iApply iProto_le_swap. iIntros (x1 x2) "/= HP1 HP2".
+    iApply iProto_le_swap. iIntros "!>" (x1 x2) "/= HP1 HP2".
     iExists TT2, TT1, (λ x2, (v2 x2, P2 x2, p x1 x2)),
       (λ x1, (v1 x1, P1 x1, p x1 x2)), x2, x1; simpl.
     do 2 (iSplit; [done|]). do 2 (iSplitR; [iApply iProto_le_refl|]). by iFrame.
@@ -773,28 +684,25 @@ Section proto.
       iRewrite "Hp2"; clear p2. iEval (rewrite !iProto_dual_message').
       rewrite iProto_le_unfold; iRight.
       iExists _, _, _, _; do 2 (iSplit; [done|]); simpl. destruct a2; simpl.
-      + iIntros (v p1d). iDestruct 1 as (p1') "[Hpc #Hp1d]".
-        iMod ("H" with "Hpc") as (p2') "[H Hpc]".
+      + iIntros "!>" (v p1d). iDestruct 1 as (p1') "[Hpc #Hp1d]".
+        iDestruct ("H" with "Hpc") as (p2') "[H Hpc]".
         iDestruct ("IH" with "H") as "H".
-        iModIntro. iExists (iProto_dual p2'). iSplitR "Hpc"; [|by auto].
-        iNext. by iRewrite "Hp1d".
-      + iIntros (v1 v2 p1d p2d).
+        iExists (iProto_dual p2'). iSplitR "Hpc"; [|by auto]. by iRewrite "Hp1d".
+      + iIntros "!>" (v1 v2 p1d p2d).
         iDestruct 1 as (p1') "[Hpc1 #Hp1d]". iDestruct 1 as (p2') "[Hpc2 #Hp2d]".
-        iMod ("H" with "Hpc2 Hpc1") as (pc1' pc2' pt) "(H1 & H2 & Hpc1 & Hpc2)".
+        iDestruct ("H" with "Hpc2 Hpc1") as (pc1' pc2' pt) "(H1 & H2 & Hpc1 & Hpc2)".
         iDestruct ("IH" with "H1") as "H1". iDestruct ("IH" with "H2") as "H2 {IH}".
-        rewrite !iProto_dual_message' /=. iModIntro. iExists _, _, (iProto_dual pt).
-        iSplitL "H2"; [iNext; by iRewrite "Hp1d"|].
-        iSplitL "H1"; [iNext; by iRewrite "Hp2d"|].
+        rewrite !iProto_dual_message' /=. iExists _, _, (iProto_dual pt).
+        iSplitL "H2"; [by iRewrite "Hp1d"|]. iSplitL "H1"; [by iRewrite "Hp2d"|].
         iSplitL "Hpc2"; simpl; auto.
     - iDestruct (iProto_le_recv_inv with "H") as (pc2) "[Hp2 H]".
       iRewrite "Hp2"; clear p2. iEval (rewrite !iProto_dual_message' /=).
       rewrite iProto_le_unfold; iRight.
       iExists _, _, _, _; do 2 (iSplit; [done|]); simpl.
-      iIntros (v p2d). iDestruct 1 as (p2') "[Hpc #Hp2d]".
-      iMod ("H" with "Hpc") as (p1') "[H Hpc]".
+      iIntros "!>" (v p2d). iDestruct 1 as (p2') "[Hpc #Hp2d]".
+      iDestruct ("H" with "Hpc") as (p1') "[H Hpc]".
       iDestruct ("IH" with "H") as "H".
-      iModIntro. iExists (iProto_dual p1'). iSplitR "Hpc"; [|by auto].
-      iNext. by iRewrite "Hp2d".
+      iExists (iProto_dual p1'). iSplitR "Hpc"; [|by auto]. by iRewrite "Hp2d".
   Qed.
 
   Lemma iProto_le_dual_l p1 p2 :
@@ -803,7 +711,6 @@ Section proto.
     iIntros "H". iEval (rewrite -(involutive iProto_dual p2)).
     by iApply iProto_le_dual.
   Qed.
-
   Lemma iProto_le_dual_r p1 p2 :
     iProto_le p2 (iProto_dual p1) -∗ iProto_le p1 (iProto_dual p2).
   Proof.
@@ -821,30 +728,28 @@ Section proto.
       iRewrite "Hp1"; clear p1.
       rewrite !iProto_app_message'. iEval (rewrite iProto_le_unfold).
       iRight. iExists _, _, _, _; do 2 (iSplit; [done|]). destruct a1; simpl.
-      + iIntros (v p24). iDestruct 1 as (p2') "[Hpc #Hp24]".
-        iMod ("H1" with "Hpc") as (p1') "[H1 Hpc]". iIntros "!>".
+      + iIntros "!>" (v p24). iDestruct 1 as (p2') "[Hpc #Hp24]".
+        iDestruct ("H1" with "Hpc") as (p1') "[H1 Hpc]".
         iExists (p1' <++> p3)%proto. iSplitR "Hpc"; [|eauto].
-        iIntros "!>". iRewrite "Hp24". by iApply ("IH" with "H1").
-      + iIntros (v1 v2 p13 p24).
+        iRewrite "Hp24". by iApply ("IH" with "H1").
+      + iIntros "!>" (v1 v2 p13 p24).
         iDestruct 1 as (p1') "[Hpc1 #Hp13]"; iDestruct 1 as (p2') "[Hpc2 #Hp24]".
-        iMod ("H1" with "Hpc1 Hpc2") as (pc1' pc2' pt) "(H1 & H1' & Hpc1 & Hpc2)".
-        iIntros "!>".
-        iExists (iProto_map_cont (flip iProto_app p3) ∘ pc1'),
-          (iProto_map_cont (flip iProto_app p3) ∘ pc2'), (pt <++> p3)%proto.
+        iDestruct ("H1" with "Hpc1 Hpc2") as (pc1' pc2' pt) "(H1 & H1' & Hpc1 & Hpc2)".
+        iExists (iProto_map_app_cont (flip iProto_app p3) ∘ pc1'),
+          (iProto_map_app_cont (flip iProto_app p3) ∘ pc2'), (pt <++> p3)%proto.
         rewrite -!iProto_app_message' /=. iSplitL "H1".
-        { iIntros "!>". iRewrite "Hp13". iApply ("IH" with "H1").
-          iApply iProto_le_refl. }
+        { iRewrite "Hp13". iApply ("IH" with "H1"). iApply iProto_le_refl. }
         iSplitL "H2 H1'".
-        { iIntros "!>". iRewrite "Hp24". iApply ("IH" with "H1' H2"). }
+        { iRewrite "Hp24". iApply ("IH" with "H1' H2"). }
         iSplitL "Hpc1"; auto.
     - iDestruct (iProto_le_recv_inv with "H1") as (pc1) "[Hp1 H1]".
       iRewrite "Hp1"; clear p1.
       rewrite !iProto_app_message'. iEval (rewrite iProto_le_unfold).
       iRight. iExists _, _, _, _; do 2 (iSplit; [done|]); simpl.
-      iIntros (v p13). iDestruct 1 as (p1') "[Hpc #Hp13]".
-      iMod ("H1" with "Hpc") as (p2'') "[H1 Hpc]". iIntros "!>".
+      iIntros "!>" (v p13). iDestruct 1 as (p1') "[Hpc #Hp13]".
+      iDestruct ("H1" with "Hpc") as (p2'') "[H1 Hpc]".
       iExists (p2'' <++> p4)%proto. iSplitR "Hpc"; [|eauto].
-      iIntros "!>". iRewrite "Hp13". by iApply ("IH" with "H1").
+      iRewrite "Hp13". by iApply ("IH" with "H1").
   Qed.
 
   (** ** Lemmas about the auxiliary definitions and invariants *)
@@ -907,12 +812,12 @@ Section proto.
       (∃ vl vsl' pc pr',
         ⌜ vsl = vl :: vsl' ⌝ ∗
         iProto_le (proto_message Recv pc) pr ∗
-        pc vl (Next pr') ∗
+        pc vl pr' ∗
         iProto_interp vsl' vsr pl pr') ∨
       (∃ vr vsr' pc pl',
         ⌜ vsr = vr :: vsr' ⌝ ∗
         iProto_le (proto_message Recv pc) pl ∗
-        pc vr (Next pl') ∗
+        pc vr pl' ∗
         iProto_interp vsl vsr' pl' pr).
   Proof.
     rewrite {1}/iProto_interp. destruct vsl as [|vl vsl]; simpl.
@@ -979,7 +884,7 @@ Section proto.
   Lemma iProto_interp_send vl pcl vsl vsr pl pr pl' :
     iProto_interp vsl vsr pl pr -∗
     iProto_le pl (proto_message Send pcl) -∗
-    pcl vl (Next pl') -∗
+    pcl vl pl' -∗
     â–·^(length vsr) iProto_interp (vsl ++ [vl]) vsr pl' pr.
   Proof.
     iIntros "H Hle". iDestruct (iProto_interp_le_l with "H Hle") as "H".
@@ -1002,10 +907,10 @@ Section proto.
     - iDestruct "H" as (vr' vsr' pc' pl'' ->) "(Hle & Hpcl' & H) /=".
       iDestruct (iProto_le_send_inv with "Hle") as (a pcl') "[Hpc Hle]".
       iDestruct (proto_message_equivI with "Hpc") as (<-) "Hpc".
-      iRewrite ("Hpc" $! vr' (Next pl'')) in "Hpcl'"; clear pc'.
-      iMod ("Hle" with "Hpcl' Hpcl")
+      iIntros "!>". iRewrite ("Hpc" $! vr' pl'') in "Hpcl'"; clear pc'.
+      iDestruct ("Hle" with "Hpcl' Hpcl")
         as (pc1 pc2 pt) "(Hpl'' & Hpl' & Hpc1 & Hpc2)".
-      iNext. iDestruct (iProto_interp_le_l with "H Hpl''") as "H".
+      iDestruct (iProto_interp_le_l with "H Hpl''") as "H".
       iDestruct ("IH" with "[%] [//] H Hpc1") as "H"; [simpl; lia|..].
       iNext. iApply iProto_interp_unfold. iRight; iRight.
       iExists vr', vsr', _, pt. iSplit; [done|]. by iFrame.
@@ -1014,7 +919,7 @@ Section proto.
   Lemma iProto_interp_recv vl vsl vsr pl pr pcr :
     iProto_interp (vl :: vsl) vsr pl pr -∗
     iProto_le pr (proto_message Recv pcr) -∗
-    ◇ ∃ pr, pcr vl (Next pr) ∗ ▷ iProto_interp vsl vsr pl pr.
+    ▷ ∃ pr, pcr vl pr ∗ iProto_interp vsl vsr pl pr.
   Proof.
     iIntros "H Hle". iDestruct (iProto_interp_le_r with "H Hle") as "H".
     clear pr. remember (length vsr) as n eqn:Hn.
@@ -1024,13 +929,14 @@ Section proto.
     - iClear "IH". iDestruct "H" as (vl' vsl' pc' pr' [= -> ->]) "(Hpr & Hpc' & Hinterp)".
       iDestruct (iProto_le_recv_inv with "Hpr") as (pc'') "[Hpc Hpr]".
       iDestruct (proto_message_equivI with "Hpc") as (_) "{Hpc} #Hpc".
-      iMod ("Hpr" $! vl' pr' with "[Hpc']") as (pr'') "[Hler Hpr]".
-      { by iRewrite -("Hpc" $! vl' (Next pr')). }
-      iModIntro. iExists pr''. iFrame "Hpr".
+      iIntros "!>".
+      iDestruct ("Hpr" $! vl' pr' with "[Hpc']") as (pr'') "[Hler Hpr]".
+      { by iRewrite -("Hpc" $! vl' pr'). }
+      iExists pr''. iFrame "Hpr".
       by iApply (iProto_interp_le_r with "Hinterp").
     - iDestruct "H" as (vr vsr' pc' pl'' ->) "(Hpl & Hpc' & Hinterp)".
-      iMod ("IH" with "[%] [//] Hinterp") as (pr) "[Hpc Hinterp]"; [simpl; lia|].
-      iModIntro. iExists pr. iFrame "Hpc".
+      iDestruct ("IH" with "[%] [//] Hinterp") as (pr) "[Hpc Hinterp]"; [simpl; lia|].
+      iIntros "!>". iExists pr. iFrame "Hpc".
       iApply iProto_interp_unfold. iRight; iRight. eauto 20 with iFrame.
   Qed.
 
@@ -1119,7 +1025,8 @@ Section proto.
     iDestruct (iProto_interp_recv with "Hinterp [Hle]") as (q) "[Hpc Hinterp]".
     { iNext. by iRewrite "Hp". }
     iMod (iProto_own_auth_update _ _ _ _ q with "H●l H◯") as "[H●l H◯]".
-    iIntros "!> !>". iMod "Hinterp". iMod "Hpc" as (x ->) "[Hpc #Hq] /=".
+    iIntros "!> !> /=".
+    iMod (bi.later_exist_except_0 with "Hpc") as (x) "(>-> & Hpc & #Hq)".
     iIntros "!>". iExists x. iSplit; [done|]. iFrame "Hpc". iSplitR "Hâ—¯".
     - iExists q, pr. iFrame. by iApply iProto_interp_flip.
     - iExists q. iIntros "{$Hâ—¯} !>". iRewrite "Hq". iApply iProto_le_refl.
@@ -1140,7 +1047,8 @@ Section proto.
     iDestruct (iProto_interp_recv with "Hinterp [Hle]") as (q) "[Hpc Hinterp]".
     { iNext. by iRewrite "Hp". }
     iMod (iProto_own_auth_update _ _ _ _ q with "H●r H◯") as "[H●r H◯]".
-    iIntros "!> !>". iMod "Hinterp". iMod "Hpc" as (x ->) "[Hpc #Hq] /=".
+    iIntros "!> !> /=".
+    iMod (bi.later_exist_except_0 with "Hpc") as (x) "(>-> & Hpc & #Hq)".
     iIntros "!>". iExists x. iSplit; [done|]. iFrame "Hpc". iSplitR "Hâ—¯".
     - iExists pl, q. iFrame.
     - iExists q. iIntros "{$Hâ—¯} !>". iRewrite "Hq". iApply iProto_le_refl.
diff --git a/theories/channel/proto_model.v b/theories/channel/proto_model.v
index af5db2faea79b978deae26c6bba5a69654a975fb..0a0a5ccc9efa23fd1850f3cb93b88504caccb914 100644
--- a/theories/channel/proto_model.v
+++ b/theories/channel/proto_model.v
@@ -8,7 +8,7 @@ Important: This file should not be used directly, but rather the wrappers in
 Dependent Separation Protocols are modeled as the solution of the following
 recursive domain equation:
 
-[proto = 1 + (action * (V → (▶ proto → PROP) → PROP))]
+[proto = 1 + (action * ▶ (V → proto → PROP))]
 
 Here, the left-hand side of the sum is used for the terminated process, while
 the right-hand side is used for the communication constructors. The type
@@ -16,10 +16,10 @@ the right-hand side is used for the communication constructors. The type
 [Recv]. Compared to having an additional sum in [proto], this makes it
 possible to factorize the code in a better way.
 
-The remainder [V → (▶ proto → PROP) → PROP)] is a predicate that ranges over
-the communicated value [V] and the tail protocol [▶ proto → PROP]. Note that in
-order to solve this recursive domain equation using Iris's COFE solver, the
-recursive occurrences of [proto] appear under the guard [â–¶].
+The remainder [▶ (V → proto → PROP)] is a predicate that ranges over the
+communicated value [V] and the tail protocol [proto]. Note that to solve this
+recursive domain equation using Iris's COFE solver, the recursive occurrence
+of [proto] appear under the later [â–¶].
 
 On top of the type [proto], we define the constructors:
 
@@ -49,9 +49,9 @@ Module Export action.
 End action.
 
 Definition proto_auxO (V : Type) (PROP : ofeT) (A : ofeT) : ofeT :=
-  optionO (prodO actionO (V -d> laterO A -n> PROP)).
+  optionO (prodO actionO (laterO (V -d> A -n> PROP))).
 Definition proto_auxOF (V : Type) (PROP : ofeT) : oFunctor :=
-  optionOF (actionO * (V -d> ▶ ∙ -n> PROP)).
+  optionOF (actionO * ▶ (V -d> ∙ -n> PROP)).
 
 Definition proto_result (V : Type) := result_2 (proto_auxOF V).
 Definition proto (V : Type) (PROPn PROP : ofeT) `{!Cofe PROPn, !Cofe PROP} : ofeT :=
@@ -77,13 +77,23 @@ Proof. apply (ofe_iso_21 proto_iso). Qed.
 Definition proto_end {V} `{!Cofe PROPn, !Cofe PROP} : proto V PROPn PROP :=
   proto_fold None.
 Definition proto_message {V} `{!Cofe PROPn, !Cofe PROP} (a : action)
-    (pc : V → laterO (proto V PROP PROPn) -n> PROP) : proto V PROPn PROP :=
-  proto_fold (Some (a, pc)).
+    (pc : V → proto V PROP PROPn -n> PROP) : proto V PROPn PROP :=
+  proto_fold (Some (a, Next pc)).
 
+Instance proto_message_contractive {V} `{!Cofe PROPn, !Cofe PROP} a n :
+  Proper (pointwise_relation V (dist_later n) ==> dist n)
+         (proto_message (PROPn:=PROPn) (PROP:=PROP) a).
+Proof.
+  intros c1 c2 Hc. rewrite /proto_message. f_equiv. do 2 constructor=>//=.
+  apply Next_contractive. by destruct n.
+Qed.
 Instance proto_message_ne {V} `{!Cofe PROPn, !Cofe PROP} a n :
   Proper (pointwise_relation V (dist n) ==> dist n)
          (proto_message (PROPn:=PROPn) (PROP:=PROP) a).
-Proof. intros c1 c2 Hc. rewrite /proto_message. f_equiv. by repeat constructor. Qed.
+Proof.
+  intros c1 c2 Hc. apply proto_message_contractive=> v.
+  by destruct n; [|apply dist_S].
+Qed.
 Instance proto_message_proper {V} `{!Cofe PROPn, !Cofe PROP} a :
   Proper (pointwise_relation V (≡) ==> (≡))
          (proto_message (PROPn:=PROPn) (PROP:=PROP) a).
@@ -94,14 +104,15 @@ Lemma proto_case {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
 Proof.
   destruct (proto_unfold p) as [[a pc]|] eqn:E; simpl in *; last first.
   - left. by rewrite -(proto_fold_unfold p) E.
-  - right. exists a, pc. by rewrite -(proto_fold_unfold p) E.
+  - right. destruct (Next_uninj pc) as [pc' Hpc]. exists a, pc'.
+    by rewrite /proto_message -Hpc -E proto_fold_unfold.
 Qed.
 Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
   Inhabited (proto V PROPn PROP) := populate proto_end.
 
 Lemma proto_message_equivI {SPROP : sbi} {V} `{!Cofe PROPn, !Cofe PROP} a1 a2 pc1 pc2 :
   proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a1 pc1 ≡ proto_message a2 pc2
-  ⊣⊢@{SPROP} ⌜ a1 = a2 ⌝ ∧ (∀ v p', pc1 v p' ≡ pc2 v p').
+  ⊣⊢@{SPROP} ⌜ a1 = a2 ⌝ ∧ ▷ (∀ v p', pc1 v p' ≡ pc2 v p').
 Proof.
   trans (proto_unfold (proto_message a1 pc1) ≡ proto_unfold (proto_message a2 pc2) : SPROP)%I.
   { iSplit.
@@ -109,7 +120,8 @@ Proof.
     - iIntros "Heq". rewrite -{2}(proto_fold_unfold (proto_message _ _)).
       iRewrite "Heq". by rewrite proto_fold_unfold. }
   rewrite /proto_message !proto_unfold_fold bi.option_equivI bi.prod_equivI /=.
-  rewrite bi.discrete_fun_equivI bi.discrete_eq. by setoid_rewrite bi.ofe_morO_equivI.
+  rewrite bi.discrete_eq bi.later_equivI bi.discrete_fun_equivI.
+  by setoid_rewrite bi.ofe_morO_equivI.
 Qed.
 Lemma proto_message_end_equivI {SPROP : sbi} {V} `{!Cofe PROPn, !Cofe PROP} a pc :
   proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a pc ≡ proto_end ⊢@{SPROP} False.
@@ -122,35 +134,65 @@ Lemma proto_end_message_equivI {SPROP : sbi} {V} `{!Cofe PROPn, !Cofe PROP} a pc
   proto_end ≡ proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a pc ⊢@{SPROP} False.
 Proof. by rewrite bi.internal_eq_sym proto_message_end_equivI. Qed.
 
-(** Functor *)
-Definition proto_cont_map `{!Cofe PROP, !Cofe PROP', !Cofe A, !Cofe B}
-    (g : PROP -n> PROP') (rec : B -n> A) :
-    (laterO A -n> PROP) -n> laterO B -n> PROP' :=
-  ofe_morO_map (laterO_map rec) g.
+(** The eliminator [proto_elim x f p] is only well-behaved if the function [f]
+is contractive *)
+Definition proto_elim {V} `{!Cofe PROPn, !Cofe PROP} {A}
+    (x : A) (f : action → (V → proto V PROP PROPn -n> PROP) → A)
+    (p : proto V PROPn PROP) : A :=
+  match proto_unfold p with None => x | Some (a, pc) => f a (later_car pc) end.
 
-Program Definition proto_map_aux {V}
-   `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
-    (g : PROP -n> PROP')
-    (rec : proto V PROP' PROPn' -n> proto V PROP PROPn) :
+Lemma proto_elim_ne {V} `{!Cofe PROPn, !Cofe PROP} {A : ofeT}
+    (x : A) (f1 f2 : action → (V → proto V PROP PROPn -n> PROP) → A) p1 p2 n :
+  (∀ a pc1 pc2, (∀ v, dist_later n (pc1 v) (pc2 v)) → f1 a pc1 ≡{n}≡ f2 a pc2) →
+  p1 ≡{n}≡ p2 →
+  proto_elim x f1 p1 ≡{n}≡ proto_elim x f2 p2.
+Proof.
+  intros Hf Hp. rewrite /proto_elim.
+  apply (_ : NonExpansive proto_unfold) in Hp
+    as [[a1 pc1] [a2 pc2] [-> ?]|]; simplify_eq/=; [|done].
+  apply Hf. destruct n; by simpl.
+Qed.
+
+Lemma proto_elim_end {V} `{!Cofe PROPn, !Cofe PROP} {A : ofeT}
+    (x : A) (f : action → (V → proto V PROP PROPn -n> PROP) → A) :
+  proto_elim x f proto_end ≡ x.
+Proof.
+  rewrite /proto_elim /proto_end.
+  pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn) (PROP:=PROP) None) as Hfold.
+  by destruct (proto_unfold (proto_fold None)) as [[??]|] eqn:E; inversion Hfold.
+Qed.
+Lemma proto_elim_message {V} `{!Cofe PROPn, !Cofe PROP} {A : ofeT}
+    (x : A) (f : action → (V → proto V PROP PROPn -n> PROP) → A)
+    `{Hf : ∀ a, Proper (pointwise_relation _ (≡) ==> (≡)) (f a)} a pc :
+  proto_elim x f (proto_message a pc) ≡ f a pc.
+Proof.
+  rewrite /proto_elim /proto_message /=.
+  pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn)
+    (PROP:=PROP) (Some (a, Next pc))) as Hfold.
+  destruct (proto_unfold (proto_fold (Some (a, Next pc))))
+    as [[??]|] eqn:E; inversion Hfold as [?? [Ha Hc]|]; simplify_eq/=.
+  by f_equiv=> v.
+Qed.
+
+(** Functor *)
+Program Definition proto_map_aux {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
+    (g : PROP -n> PROP') (rec : proto V PROP' PROPn' -n> proto V PROP PROPn) :
     proto V PROPn PROP -n> proto V PROPn' PROP' := λne p,
-  match proto_unfold p return _ with
-  | None => proto_end
-  | Some (a, c) => proto_message a (proto_cont_map g rec ∘ c)
-  end.
+  proto_elim proto_end (λ a pc, proto_message a (λ v, g ◎ pc v ◎ rec)) p.
 Next Obligation.
   intros V PROPn ? PROPn' ? PROP ? PROP' ? g rec n p1 p2 Hp.
-  apply (ofe_mor_ne _ _ proto_unfold) in Hp.
-  destruct Hp as [[??][??] [-> ?]|]; simplify_eq/=; last done.
-  f_equiv=> v /=. by f_equiv.
+  apply proto_elim_ne=> // a pc1 pc2 Hpc.
+  apply proto_message_contractive; destruct n as [|n]=> // v p' /=.
+  do 2 f_equiv. apply Hpc.
 Qed.
+
 Instance proto_map_aux_contractive {V}
    `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'} (g : PROP -n> PROP') :
   Contractive (proto_map_aux (V:=V) (PROPn:=PROPn) (PROPn':=PROPn') g).
 Proof.
-  intros n rec1 rec2 Hrec p. simpl.
-  destruct (proto_unfold p) as [[a c]|]; last done.
-  f_equiv=> v p' /=. do 2 f_equiv. apply Next_contractive.
-  destruct n as [|n]=> //=.
+  intros n rec1 rec2 Hrec p. simpl. apply proto_elim_ne=> // a pc1 pc2 Hpc.
+  apply proto_message_contractive; destruct n as [|n]=> // v p'; simpl in *.
+  by rewrite (Hrec p') (Hpc _ (rec2 _)).
 Qed.
 
 Definition proto_map_aux_2 {V}
@@ -167,7 +209,6 @@ Proof.
   intros n rec1 rec2 Hrec. rewrite /proto_map_aux_2.
   f_equiv. by apply proto_map_aux_contractive.
 Qed.
-
 Definition proto_map {V}
    `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
     (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
@@ -189,44 +230,33 @@ Qed.
 Lemma proto_map_end {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
     (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
   proto_map (V:=V) gn g proto_end ≡ proto_end.
-Proof.
-  rewrite proto_map_unfold /proto_end /=.
-  pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn) (PROP:=PROP) None) as Hfold.
-  by destruct (proto_unfold (proto_fold None)) as [[??]|] eqn:E; inversion Hfold.
-Qed.
+Proof. by rewrite proto_map_unfold /proto_map_aux /= proto_elim_end. Qed.
 Lemma proto_map_message {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
-    (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') a c :
-  proto_map (V:=V) gn g (proto_message a c)
-  ≡ proto_message a (proto_cont_map g (proto_map g gn) ∘ c).
+    (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') a pc :
+  proto_map (V:=V) gn g (proto_message a pc)
+  ≡ proto_message a (λ v, g ◎ pc v ◎ proto_map g gn).
 Proof.
-  rewrite proto_map_unfold /proto_message /=.
-  pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn)
-    (PROP:=PROP) (Some (a, c))) as Hfold.
-  destruct (proto_unfold (proto_fold (Some (a, c))))
-    as [[??]|] eqn:E; inversion Hfold as [?? [Ha Hc]|]; simplify_eq/=.
-  rewrite /proto_message. do 3 f_equiv. intros v=> /=.
-  apply equiv_dist=> n. f_equiv. by apply equiv_dist.
+  rewrite proto_map_unfold /proto_map_aux /=.
+  apply: proto_elim_message=> a' pc1 pc2 Hpc; f_equiv; solve_proper.
 Qed.
 
 Lemma proto_map_ne {V}
     `{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hc:!Cofe PROP, Hc':!Cofe PROP'}
     (gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p n :
-  (∀ x, gn1 x ≡{n}≡ gn2 x) → (∀ x, g1 x ≡{n}≡ g2 x) →
+  gn1 ≡{n}≡ gn2 → g1 ≡{n}≡ g2 →
   proto_map (V:=V) gn1 g1 p ≡{n}≡ proto_map (V:=V) gn2 g2 p.
 Proof.
   revert PROPn Hcn PROPn' Hcn' PROP Hc PROP' Hc' gn1 gn2 g1 g2 p.
   induction (lt_wf n) as [n _ IH]=>
     PROPn ? PROPn' ? PROP ? PROP' ? gn1 gn2 g1 g2 p Hgn Hg /=.
-  destruct (proto_case p) as [->|(a & c & ->)].
-  - by rewrite !proto_map_end.
-  - rewrite !proto_map_message /=. f_equiv=> v /=. f_equiv; last done.
-    intros p'. apply Next_contractive. destruct n as [|n]=> //=.
-    apply IH; first lia; auto using dist_S.
+  destruct (proto_case p) as [->|(a & pc & ->)]; [by rewrite !proto_map_end|].
+  rewrite !proto_map_message /=.
+  apply proto_message_contractive; destruct n as [|n]=> // v p' /=.
+  rewrite (dist_S _ _ _ (Hg _)) IH //; auto using dist_S with lia.
 Qed.
 Lemma proto_map_ext {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
     (gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p :
-  (∀ x, gn1 x ≡ gn2 x) → (∀ x, g1 x ≡ g2 x) →
-  proto_map (V:=V) gn1 g1 p ≡ proto_map (V:=V) gn2 g2 p.
+  gn1 ≡ gn2 → g1 ≡ g2 → proto_map (V:=V) gn1 g1 p ≡ proto_map (V:=V) gn2 g2 p.
 Proof.
   intros Hgn Hg. apply equiv_dist=> n.
   apply proto_map_ne=> // ?; by apply equiv_dist.
@@ -236,11 +266,10 @@ Lemma proto_map_id {V} `{Hcn:!Cofe PROPn, Hc:!Cofe PROP} (p : proto V PROPn PROP
 Proof.
   apply equiv_dist=> n. revert PROPn Hcn PROP Hc p.
   induction (lt_wf n) as [n _ IH]=> PROPn ? PROP ? p /=.
-  destruct (proto_case p) as [->|(a & c & ->)].
-  - by rewrite !proto_map_end.
-  - rewrite !proto_map_message /=. f_equiv=> v c' /=. f_equiv.
-    apply Next_contractive. destruct n as [|n]=> //=.
-    apply IH; first lia; auto using dist_S.
+  destruct (proto_case p) as [->|(a & pc & ->)]; [by rewrite !proto_map_end|].
+  rewrite !proto_map_message /=.
+  apply proto_message_contractive; destruct n as [|n]=> // v p' /=.
+  by rewrite IH; last lia.
 Qed.
 Lemma proto_map_compose {V}
    `{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hcn'':!Cofe PROPn'',
@@ -253,11 +282,10 @@ Proof.
     PROP Hc PROP' Hc' PROP'' Hc'' gn1 gn2 g1 g2 p.
   induction (lt_wf n) as [n _ IH]=> PROPn ? PROPn' ? PROPn'' ?
     PROP ? PROP' ? PROP'' ? gn1 gn2 g1 g2 p /=.
-  destruct (proto_case p) as [->|(a & c & ->)].
-  - by rewrite !proto_map_end.
-  - rewrite !proto_map_message /=. f_equiv=> v c' /=. do 3 f_equiv.
-    apply Next_contractive. destruct n as [|n]=> //=.
-    apply IH; first lia; auto using dist_S.
+  destruct (proto_case p) as [->|(a & c & ->)]; [by rewrite !proto_map_end|].
+  rewrite !proto_map_message /=.
+  apply proto_message_contractive; destruct n as [|n]=> // v p' /=.
+  by rewrite IH; last lia.
 Qed.
 
 Program Definition protoOF (V : Type) (Fn F : oFunctor)
@@ -288,7 +316,6 @@ Instance protoOF_contractive (V : Type) (Fn F : oFunctor)
   oFunctorContractive (protoOF V Fn F).
 Proof.
   intros ?? A1 ? A2 ? B1 ? B2 ? n f g Hfg p; simpl in *.
-  apply proto_map_ne=> //= y.
-  - destruct n; [|destruct Hfg]; by apply oFunctor_map_contractive.
-  - destruct n; [|destruct Hfg]; by apply oFunctor_map_contractive.
+  apply proto_map_ne=> //= y;
+    [destruct n; [|destruct Hfg]; by apply oFunctor_map_contractive..].
 Qed.
diff --git a/theories/logrel/examples/double.v b/theories/logrel/examples/double.v
index 64067af89ce69bf7686ea28ce71f1590fd6c1181..ded8b10d35d2992cc482e4efd175a0619924670a 100755
--- a/theories/logrel/examples/double.v
+++ b/theories/logrel/examples/double.v
@@ -7,7 +7,7 @@ From actris.logrel Require Export types subtyping.
 
 Definition prog : val := λ: "c",
   let: "lock" := newlock #() in
-  let: "p" := (
+  (
     acquire "lock";;
     let: "x1" := recv "c" in
     release "lock";;
@@ -17,16 +17,14 @@ Definition prog : val := λ: "c",
     let: "x2" := recv "c" in
     release "lock";;
     "x2"
-  ) in "p".
+  ).
 
-Section GhostState.
-  Class fracG Σ := { frac_inG :> inG Σ fracR }.
-  Definition fracΣ : gFunctors := #[GFunctor fracR].
-  Instance subG_fracΣ {Σ} : subG fracΣ Σ → fracG Σ.
-  Proof. solve_inG. Qed.
-End GhostState.
+Class fracG Σ := { frac_inG :> inG Σ fracR }.
+Definition fracΣ : gFunctors := #[GFunctor fracR].
+Instance subG_fracΣ {Σ} : subG fracΣ Σ → fracG Σ.
+Proof. solve_inG. Qed.
 
-Section Double.
+Section double.
   Context `{heapG Σ, chanG Σ, fracG Σ, spawnG Σ}.
 
   Definition prog_prot : iProto Σ :=
@@ -38,21 +36,19 @@ Section Double.
      (own γ 1%Qp ∗ c ↣ END))%I.
 
   Lemma wp_prog (c : val):
-    {{{ ▷ (c ↣ prog_prot) }}}
+    {{{ ▷ c ↣ prog_prot }}}
       prog c
-    {{{ v, RET v; ∃ k1 k2 : Z, ⌜v = (#k1, #k2)%V⌝ }}}.
+    {{{ (k1 k2 : Z), RET (#k1, #k2); True }}}.
   Proof.
     iIntros (Φ) "Hc HΦ".
     rewrite /prog.
-    iMod (own_alloc 1%Qp) as (γ) "[Hcredit1 Hcredit2]".
-    { done. }
+    iMod (own_alloc 1%Qp) as (γ) "[Hcredit1 Hcredit2]"; [done|].
     (* Create lock *)
     wp_apply (newlock_spec (chan_inv c γ) with "[Hc]").
     { iLeft. iFrame "Hc". }
     iIntros (lk γlk) "#Hlock".
     wp_pures.
     (* Fork into two threads *)
-    wp_bind (par _ _).
     wp_apply (wp_par (λ v, ∃ k : Z, ⌜v = #k⌝)%I (λ v, ∃ k : Z, ⌜v = #k⌝)%I
                 with "[Hcredit1] [Hcredit2]").
     - (* Acquire lock *)
@@ -72,8 +68,7 @@ Section Double.
         iIntros "_". wp_pures.
         eauto.
       + iDestruct "Hc" as "[Hcredit2 Hc]".
-        iExFalso. iDestruct (own_valid_2 with "Hcredit1 Hcredit2") as "%".
-        done.
+        by iDestruct (own_valid_2 with "Hcredit1 Hcredit2") as %[].
     - (* Acquire lock *)
       wp_apply (acquire_spec with "Hlock").
       iIntros "[Hlocked Hc]". wp_pures.
@@ -91,38 +86,26 @@ Section Double.
         iIntros "_". wp_pures.
         eauto.
       + iDestruct "Hc" as "[Hcredit1 Hc]".
-        iExFalso. iDestruct (own_valid_2 with "Hcredit1 Hcredit2") as "%".
-        done.
-    - iIntros (x1 x2) "[Hx1 Hx2]".
-      iModIntro. wp_pures.
-      iApply "HΦ".
-      iDestruct "Hx1" as (k1) "->".
-      iDestruct "Hx2" as (k2) "->".
-      by iExists k1, k2.
+        by iDestruct (own_valid_2 with "Hcredit1 Hcredit2") as %[].
+    - iIntros (?? [[x1 ->] [x2 ->]]) "!>". wp_pures. by iApply "HΦ".
   Qed.
 
   Lemma prog_typed :
-    ⊢ (∅ ⊨ prog : chan (<??> lty_int; <??> lty_int; END) ⊸ (lty_int * lty_int))%I.
+    ⊢ ∅ ⊨ prog : chan (<??> lty_int; <??> lty_int; END) ⊸ lty_int * lty_int.
   Proof.
     iIntros (vs) "!> HΓ /=".
     iApply wp_value.
     iIntros (c) "Hc".
-    iApply (wp_prog with "[Hc]")=> //=.
-    {
-      iApply (iProto_mapsto_le _ (<??> lty_int; <??> lty_int; END)%lsty with "Hc").
+    iApply (wp_prog with "[Hc]").
+    { iApply (iProto_mapsto_le _ (<??> lty_int; <??> lty_int; END)%lsty with "Hc").
       iApply iProto_le_recv.
-      iIntros "!> !>" (v) ">H !>".
-      iDestruct "H" as (x) "->"=> /=.
-      iExists _. do 2 iSplit=> //.
+      iIntros "!> !> !>" (? [x ->]).
+      iExists _. do 2 (iSplit; [done|]).
       iApply iProto_le_recv.
-      iIntros "!>" (v) ">H !>".
-      iDestruct "H" as (y) "->"=> /=.
-      iExists _. do 2 iSplit=> //.
-      iApply iProto_le_refl.
-    }
-    iIntros "!>" (v) "H".
-    iDestruct "H" as (k1 k2) "->".
-    iExists _, _. iSplit=> //. eauto.
+      iIntros "!>" (? [y ->]).
+      iExists _. do 2 (iSplit; [done|]).
+      iApply iProto_le_refl. }
+    iIntros "!>" (k1 k2 _).
+    iExists _, _. iSplit; first done. eauto.
   Qed.
-
-End Double.
+End double.
diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index f315b9689b5dd1d2cc4240e0e342dcb614a2a46d..6c0d4f0e87c8a4cdb9d4a76efba7a96ab6d11b3e 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -183,9 +183,7 @@ Section subtype.
     ▷ (A2 <: A1) -∗ ▷ (S1 <s: S2) -∗
     (<!!> A1 ; S1) <s: (<!!> A2 ; S2).
   Proof.
-    iIntros "#HAle #HPle !>".
-    iApply iProto_le_send=> /=.
-    iIntros (x) "H !>".
+    iIntros "#HAle #HPle !>". iApply iProto_le_send; iIntros "!> /=" (x) "H".
     iDestruct ("HAle" with "H") as "H".
     eauto with iFrame.
   Qed.
@@ -194,9 +192,7 @@ Section subtype.
     ▷ (A1 <: A2) -∗ ▷ (S1 <s: S2) -∗
     (<??> A1 ; S1) <s: (<??> A2 ; S2).
   Proof.
-    iIntros "#HAle #HPle !>".
-    iApply iProto_le_recv; simpl.
-    iIntros (x) "H !>".
+    iIntros "#HAle #HSle !>". iApply iProto_le_recv; iIntros "!> /=" (x) "H".
     iDestruct ("HAle" with "H") as "H".
     eauto with iFrame.
   Qed.
@@ -204,15 +200,13 @@ Section subtype.
   Lemma lsty_le_swap (A1 A2 : lty Σ) (P : lsty Σ) :
     ⊢ (<??> A1 ; <!!> A2 ; P) <s: (<!!> A2 ; <??> A1 ; P).
   Proof.
-    iIntros "!>".
-    iApply iProto_le_swap. iIntros (x1 x2) "/= HS1 HS2".
+    iIntros "!>". iApply iProto_le_swap. iIntros "!>" (x1 x2) "/= HS1 HS2".
     iExists _, _,
       (tele_app (TT:=[tele _]) (λ x2, (x2, A2 x2, (P:iProto Σ)))),
       (tele_app (TT:=[tele _]) (λ x1, (x1, A1 x1, (P:iProto Σ)))),
       x2, x1; simpl.
     do 2 (iSplit; [done|]).
     iFrame "HS1 HS2".
-    iModIntro.
     do 2 (iSplitR; [iApply iProto_le_refl|]). by iFrame.
   Qed.
 
@@ -220,15 +214,11 @@ Section subtype.
     (▷ [∗ map] i ↦ S1;S2 ∈ Ps1; Ps2, S1 <s: S2) -∗
     lsty_select Ps1 <s: lsty_select Ps2.
   Proof.
-    iIntros "#H1 !>".
-    iApply iProto_le_send; simpl.
-    iIntros (x) ">H !>"; iDestruct "H" as %Hsome.
-    iExists x. iSplit=> //. iSplit.
-    - iNext.
-      iDestruct (big_sepM2_forall with "H1") as "[% _]".
+    iIntros "#H1 !>". iApply iProto_le_send; iIntros "!>" (x Hsome).
+    iExists x. iSplit; first done. iSplit.
+    - iDestruct (big_sepM2_forall with "H1") as "[% _]".
       iPureIntro. naive_solver.
-    - iNext.
-      iDestruct (big_sepM2_forall with "H1") as "[% H]".
+    - iDestruct (big_sepM2_forall with "H1") as "[% H]".
       iApply ("H" with "[] []").
       + iPureIntro. apply lookup_lookup_total; naive_solver.
       + iPureIntro. by apply lookup_lookup_total.
@@ -238,14 +228,10 @@ Section subtype.
     Ps2 ⊆ Ps1 →
     ⊢ lsty_select Ps1 <s: lsty_select Ps2.
   Proof.
-    iIntros (Hsub) "!>".
-    iApply iProto_le_send; simpl.
-    iIntros (x) ">% !> /=".
-    iExists _. iSplit; first done.
-    iSplit.
-    { iNext. iPureIntro. by eapply lookup_weaken_is_Some. }
-    iNext.
-    destruct H1 as [P H1].
+    iIntros (Hsub) "!>". iApply iProto_le_send; iIntros "!>" (x Hsome).
+    iExists _. iSplit; first done. iSplit.
+    { iPureIntro. by eapply lookup_weaken_is_Some. }
+    destruct Hsome as [P H1].
     assert (Ps1 !! x = Some P) by eauto using lookup_weaken.
     rewrite (lookup_total_correct Ps1 x P) //.
     rewrite (lookup_total_correct Ps2 x P) //.
@@ -256,14 +242,11 @@ Section subtype.
     (▷ [∗ map] i ↦ S1;S2 ∈ Ps1; Ps2, S1 <s: S2) -∗
     lsty_branch Ps1 <s: lsty_branch Ps2.
   Proof.
-    iIntros "#H1 !>". iApply iProto_le_recv.
-    iIntros (x) ">H !>"; iDestruct "H" as %Hsome.
+    iIntros "#H1 !>". iApply iProto_le_recv; iIntros "!>" (x Hsome).
     iExists x. iSplit; first done. iSplit.
-    - iNext.
-      iDestruct (big_sepM2_forall with "H1") as "[% _]".
+    - iDestruct (big_sepM2_forall with "H1") as "[% _]".
       iPureIntro. by naive_solver.
-    - iNext.
-      iDestruct (big_sepM2_forall with "H1") as "[% H]".
+    - iDestruct (big_sepM2_forall with "H1") as "[% H]".
       iApply ("H" with "[] []").
       + iPureIntro. by apply lookup_lookup_total.
       + iPureIntro. by apply lookup_lookup_total; naive_solver.
@@ -273,14 +256,10 @@ Section subtype.
     Ps1 ⊆ Ps2 →
     ⊢ lsty_branch Ps1 <s: lsty_branch Ps2.
   Proof.
-    iIntros (Hsub) "!>".
-    iApply iProto_le_recv; simpl.
-    iIntros (x) ">% !> /=".
-    iExists _. iSplit; first done.
-    iSplit.
-    { iNext. iPureIntro. by eapply lookup_weaken_is_Some. }
-    iNext.
-    destruct H1 as [P ?].
+    iIntros (Hsub) "!>". iApply iProto_le_recv; iIntros "!>" (x Hsome).
+    iExists _. iSplit; first done. iSplit.
+    { iPureIntro. by eapply lookup_weaken_is_Some. }
+    destruct Hsome as [P ?].
     assert (Ps2 !! x = Some P) by eauto using lookup_weaken.
     rewrite (lookup_total_correct Ps1 x P) //.
     rewrite (lookup_total_correct Ps2 x P) //.