From f672691823055165145cc2dba5ea4cd7d771542d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 26 Mar 2020 14:22:27 +0100
Subject: [PATCH] Model that does not use subsingletons + prove iProto_le_app.

---
 theories/channel/proto.v       | 353 ++++++++++++++++++++++++---------
 theories/channel/proto_model.v | 269 +++++++++----------------
 2 files changed, 353 insertions(+), 269 deletions(-)

diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 7e62cb5..542b42d 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -29,6 +29,7 @@ From iris.program_logic Require Import language.
 From iris.proofmode Require Import tactics.
 From iris.base_logic Require Import lib.own.
 From actris.channel Require Import proto_model.
+Set Default Proof Using "Type".
 Export action.
 
 (** * Setup of Iris's cameras *)
@@ -56,11 +57,11 @@ 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 f, ∃ x : TT,
+  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 ∗
-    f (Next (pc x).2))%I.
+    p' ≡ Next (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).
@@ -145,8 +146,52 @@ Notation "<?> 'MSG' v ; p" :=
 Notation "'END'" := iProto_end : proto_scope.
 
 (** * Operations *)
-Definition iProto_dual {Σ V} (p : iProto Σ V) : iProto Σ V :=
-  proto_map action_dual cid cid p.
+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.
+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.
+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.
+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).
+Qed.
+
+Definition iProto_map_app {Σ V} (f : action → action)
+    (p2 : iProto Σ V) : iProto Σ V -n> iProto Σ V :=
+  fixpoint (iProto_map_app_aux f p2).
+
+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 := iProto_app_aux.(unseal).
+Definition iProto_app_eq : @iProto_app = @iProto_app_def := iProto_app_aux.(seal_eq).
+Arguments iProto_app {_ _} _%proto _%proto.
+Instance: Params (@iProto_app) 2 := {}.
+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 := iProto_dual_aux.(unseal).
+Definition iProto_dual_eq :
+  @iProto_dual = @iProto_dual_def := iProto_dual_aux.(seal_eq).
 Arguments iProto_dual {_ _} _%proto.
 Instance: Params (@iProto_dual) 2 := {}.
 Definition iProto_dual_if {Σ V} (d : bool) (p : iProto Σ V) : iProto Σ V :=
@@ -154,17 +199,8 @@ Definition iProto_dual_if {Σ V} (d : bool) (p : iProto Σ V) : iProto Σ V :=
 Arguments iProto_dual_if {_ _} _ _%proto.
 Instance: Params (@iProto_dual_if) 3 := {}.
 
-Definition iProto_app {Σ V} (p1 p2 : iProto Σ V) : iProto Σ V := proto_app p1 p2.
-Arguments iProto_app {_ _} _%proto _%proto.
-Instance: Params (@iProto_app) 2 := {}.
-Infix "<++>" := iProto_app (at level 60) : proto_scope.
-
-(** * Auxiliary definitions and invariants *)
-Definition proto_eq_next {Σ V} (p : iProto Σ V) : laterO (iProto Σ V) -n> iPropO Σ :=
-  OfeMor (sbi_internal_eq (Next p)).
-
-(*
-The definition [iProto_le] generalizes the following inductive definition
+(** * Protocol entailment *)
+(* The definition [iProto_le] generalizes the following inductive definition
 for subtyping on session types:
 
                  p1 <: p2           p1 <: p2
@@ -191,19 +227,19 @@ Definition iProto_le_pre {Σ V}
     p2 ≡ proto_message a2 pc2 ∗
     match a1, a2 with
     | Recv, Recv =>
-       ∀ v p1', pc1 v (proto_eq_next p1') -∗
-         ◇ ∃ p2', ▷ rec p1' p2' ∗ pc2 v (proto_eq_next p2')
+       ∀ v p1', pc1 v (Next p1') -∗
+         ◇ ∃ p2', ▷ rec p1' p2' ∗ pc2 v (Next p2')
     | Send, Send =>
-       ∀ v p2', pc2 v (proto_eq_next p2') -∗
-         ◇ ∃ p1', ▷ rec p1' p2' ∗ pc1 v (proto_eq_next p1')
+       ∀ v p2', pc2 v (Next p2') -∗
+         ◇ ∃ p1', ▷ rec p1' p2' ∗ pc1 v (Next p1')
     | Recv, Send =>
        ∀ v1 v2 p1' p2',
-         pc1 v1 (proto_eq_next p1') -∗ pc2 v2 (proto_eq_next 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 (proto_eq_next pt) ∗
-           pc2' v1 (proto_eq_next pt)
+           pc1' v2 (Next pt) ∗
+           pc2' v1 (Next pt)
     | Send, Recv => False
     end.
 Instance iProto_le_pre_ne {Σ V} (rec : iProto Σ V → iProto Σ V → iProp Σ) :
@@ -220,7 +256,8 @@ Proof.
   intros n rec1 rec2 Hrec p1 p2. rewrite /iProto_le_pre' /iProto_le_pre /=.
   by repeat (f_contractive || f_equiv).
 Qed.
-Definition iProto_le {Σ V} (p1 p2 : iProto Σ V) : iProp Σ := fixpoint iProto_le_pre' p1 p2.
+Definition iProto_le {Σ V} (p1 p2 : iProto Σ V) : iProp Σ :=
+  fixpoint iProto_le_pre' p1 p2.
 Arguments iProto_le {_ _} _%proto _%proto.
 Instance: Params (@iProto_le) 2 := {}.
 
@@ -236,12 +273,12 @@ Fixpoint iProto_interp_aux {Σ V} (n : nat)
      (∃ vl vsl' pc p2',
        ⌜ vsl = vl :: vsl' ⌝ ∗
        iProto_le (proto_message Recv pc) pr ∗
-       pc vl (proto_eq_next p2') ∗
+       pc vl (Next 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 (proto_eq_next p1') ∗
+       pc vr (Next p1') ∗
        iProto_interp_aux n vsl vsr' p1' pr)
   end.
 Definition iProto_interp {Σ V} (vsl vsr : list V) (pl pr : iProto Σ V) : iProp Σ :=
@@ -272,7 +309,7 @@ Definition side_elim {A} (s : side) (l r : A) : A :=
   match s with Left => l | Right => r end.
 
 Definition iProto_unfold {Σ V} (p : iProto Σ V) : proto V (iPrePropO Σ) (iPrePropO Σ) :=
-  proto_map id iProp_fold iProp_unfold p.
+  proto_map iProp_fold iProp_unfold p.
 Definition iProto_own_frag `{!protoG Σ V} (γ : proto_name) (s : side)
     (p : iProto Σ V) : iProp Σ :=
   own (side_elim s proto_l_name proto_r_name γ) (◯E (Next (iProto_unfold p))).
@@ -334,60 +371,103 @@ Section proto.
 
   (** ** Dual *)
   Global Instance iProto_dual_ne : NonExpansive (@iProto_dual Σ V).
-  Proof. solve_proper. Qed.
+  Proof. rewrite iProto_dual_eq. solve_proper. Qed.
   Global Instance iProto_dual_proper : Proper ((≡) ==> (≡)) (@iProto_dual Σ V).
   Proof. apply (ne_proper _). Qed.
   Global Instance iProto_dual_if_ne d : NonExpansive (@iProto_dual_if Σ V d).
   Proof. solve_proper. Qed.
-  Global Instance iProto_dual_if_proper d : Proper ((≡) ==> (≡)) (@iProto_dual_if Σ V d).
+  Global Instance iProto_dual_if_proper d :
+    Proper ((≡) ==> (≡)) (@iProto_dual_if Σ V d).
   Proof. apply (ne_proper _). Qed.
 
-  Global Instance iProto_dual_involutive : Involutive (≡) (@iProto_dual Σ V).
+  Lemma iProto_dual_end' : iProto_dual (Σ:=Σ) (V:=V) proto_end ≡ proto_end.
   Proof.
-    intros p. rewrite /iProto_dual -proto_map_compose -{2}(proto_map_id p).
-    apply: proto_map_ext=> //. by intros [].
+    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.
+  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).
+  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.
   Qed.
 
   Lemma iProto_dual_end : iProto_dual (Σ:=Σ) (V:=V) END ≡ END%proto.
-  Proof. by rewrite iProto_end_eq /iProto_dual proto_map_end. Qed.
+  Proof. rewrite iProto_end_eq. apply iProto_dual_end'. Qed.
 
   Lemma iProto_dual_message {TT} a (pc : TT → V * iProp Σ * iProto Σ V) :
     iProto_dual (iProto_message a pc)
     ≡ iProto_message (action_dual a) (prod_map id iProto_dual ∘ pc).
   Proof.
-    rewrite /iProto_dual iProto_message_eq /iProto_message_def proto_map_message.
-    by f_equiv=> v f /=.
+    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".
+    - iDestruct 1 as (x ->) "[Hpc Hpd]"; auto 10.
   Qed.
 
-  (** Helpers for duals *)
-  Global Instance proto_eq_next_ne : NonExpansive (proto_eq_next (Σ:=Σ) (V:=V)).
-  Proof. solve_proper. Qed.
-  Global Instance proto_eq_next_proper :
-    Proper ((≡) ==> (≡)) (proto_eq_next (Σ:=Σ) (V:=V)).
-  Proof. solve_proper. Qed.
-
-  Lemma proto_eq_next_dual p :
-    ofe_mor_map (laterO_map (proto_map action_dual cid cid)) cid
-      (proto_eq_next (iProto_dual p)) ≡ proto_eq_next p.
+  Global Instance iProto_dual_involutive : Involutive (≡) (@iProto_dual Σ V).
   Proof.
-    intros lp. iSplit; iIntros "Hlp /="; last by iRewrite -"Hlp".
-    destruct (Next_uninj lp) as [p' ->].
-    rewrite /later_map /= !bi.later_equivI. iNext.
-    rewrite -{2}(involutive iProto_dual p) -{2}(involutive iProto_dual p').
-    by iRewrite "Hlp".
+    intros p. apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
+    iLöb as "IH" forall (p). destruct (proto_case p) as [->|(a&pc&->)].
+    { by rewrite !iProto_dual_end'. }
+    rewrite !iProto_dual_message' involutive.
+    iApply proto_message_equivI; iSplit; [done|]; iIntros (v p') "/=".
+    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'').
   Qed.
 
-  Lemma proto_eq_next_dual' p :
-    ofe_mor_map (laterO_map (proto_map action_dual cid cid)) cid (proto_eq_next p) ≡
-    proto_eq_next (iProto_dual p).
+  (** ** 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.
+  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).
   Proof.
-    rewrite -(proto_eq_next_dual (iProto_dual p))=> lp /=.
-    by rewrite involutive.
+    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.
   Qed.
 
-  (** ** Append *)
   Global Instance iProto_app_ne : NonExpansive2 (@iProto_app Σ V).
-  Proof. apply _. Qed.
+  Proof.
+    assert (∀ n, Proper (dist n ==> (=) ==> dist n) (@iProto_app Σ V)).
+    { intros n p1 p1' Hp1 p2 p2' <-. by rewrite iProto_app_eq /iProto_app_def Hp1. }
+    assert (Proper ((≡) ==> (=) ==> (≡)) (@iProto_app Σ V)).
+    { intros p1 p1' Hp1 p2 p2' <-. by rewrite iProto_app_eq /iProto_app_def Hp1. }
+    intros n p1 p1' Hp1 p2 p2' Hp2. rewrite Hp1. clear p1 Hp1.
+    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.
+  Qed.
   Global Instance iProto_app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@iProto_app Σ V).
   Proof. apply (ne_proper_2 _). Qed.
 
@@ -395,24 +475,62 @@ Section proto.
     (iProto_message a pc <++> p2)%proto
     ≡ iProto_message a (prod_map id (flip iProto_app p2) ∘ pc).
   Proof.
-    rewrite /iProto_app iProto_message_eq /iProto_message_def proto_app_message.
-    by f_equiv=> v f /=.
+    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'".
+    - iDestruct 1 as (x ->) "[Hpc Hps]". auto 10.
   Qed.
 
   Global Instance iProto_app_end_l : LeftId (≡) END%proto (@iProto_app Σ V).
-  Proof.
-    intros p. by rewrite iProto_end_eq /iProto_end_def /iProto_app proto_app_end_l.
-  Qed.
+  Proof. intros p. by rewrite iProto_end_eq /iProto_end_def iProto_app_end'. Qed.
   Global Instance iProto_app_end_r : RightId (≡) END%proto (@iProto_app Σ V).
   Proof.
-    intros p. by rewrite iProto_end_eq /iProto_end_def /iProto_app proto_app_end_r.
+    rewrite iProto_end_eq /iProto_end_def.
+    intros p. apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
+    iLöb as "IH" forall (p). destruct (proto_case p) as [->|(a&pc&->)].
+    { 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'').
   Qed.
   Global Instance iProto_app_assoc : Assoc (≡) (@iProto_app Σ V).
-  Proof. intros p1 p2 p3. by rewrite /iProto_app proto_app_assoc. Qed.
+  Proof.
+    intros p1 p2 p3. apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
+    iLöb as "IH" forall (p1). destruct (proto_case p1) as [->|(a&pc&->)].
+    { by rewrite !iProto_app_end'. }
+    rewrite !iProto_app_message'.
+    iApply proto_message_equivI; iSplit; [done|]; iIntros (v p123) "/=".
+    iApply prop_ext; iIntros "!>". iSplit.
+    - iDestruct 1 as (p1') "[H #Hp']".
+      iExists (p1' <++> p2)%proto. iSplitL; [by auto|].
+      iRewrite "Hp'". iNext. 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').
+  Qed.
 
   Lemma iProto_dual_app p1 p2 :
     iProto_dual (p1 <++> p2) ≡ (iProto_dual p1 <++> iProto_dual p2)%proto.
-  Proof. by rewrite /iProto_dual /iProto_app proto_map_app. Qed.
+  Proof.
+    apply (uPred.internal_eq_soundness (M:=iResUR Σ)).
+    iLöb as "IH" forall (p1 p2). destruct (proto_case p1) as [->|(a&pc&->)].
+    { 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.
+    - 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".
+    - 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).
+  Qed.
 
   (** ** Protocol entailment **)
   Global Instance iProto_le_ne : NonExpansive2 (@iProto_le Σ V).
@@ -445,16 +563,16 @@ Section proto.
       p1 ≡ proto_message a1 pc1 ∗
       match a1 with
       | Send =>
-         ∀ v p2', pc2 v (proto_eq_next p2') -∗
-           ◇ ∃ p1', ▷ iProto_le p1' p2' ∗ pc1 v (proto_eq_next p1')
+         ∀ v p2', pc2 v (Next p2') -∗
+           ◇ ∃ p1', ▷ iProto_le p1' p2' ∗ pc1 v (Next p1')
       | Recv =>
          ∀ v1 v2 p1' p2',
-           pc1 v1 (proto_eq_next p1') -∗ pc2 v2 (proto_eq_next 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 (proto_eq_next pt) ∗
-             pc2' v1 (proto_eq_next pt)
+             pc1' v2 (Next pt) ∗
+             pc2' v1 (Next pt)
       end.
   Proof.
     rewrite iProto_le_unfold. iIntros "[[_ Heq]|H]".
@@ -462,15 +580,15 @@ 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 (proto_eq_next p2')).
-    - iIntros (v1 v2 p1' p2'). by iRewrite ("Hpc" $! v2 (proto_eq_next p2')).
+    - iIntros (v p2'). by iRewrite ("Hpc" $! v (Next p2')).
+    - iIntros (v1 v2 p1' p2'). by iRewrite ("Hpc" $! v2 (Next 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 (proto_eq_next p1') -∗
-        ◇ ∃ p2', ▷ iProto_le p1' p2' ∗ pc2 v (proto_eq_next p2').
+      ∀ v p1', pc1 v (Next p1') -∗
+        ◇ ∃ p2', ▷ iProto_le p1' p2' ∗ pc2 v (Next p2').
   Proof.
     rewrite iProto_le_unfold. iIntros "[[_ Heq]|H]".
     { by iDestruct (proto_message_end_equivI with "Heq") as %[]. }
@@ -478,7 +596,7 @@ Section proto.
     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 (proto_eq_next p2')).
+    iExists p2'. iFrame "Hle". by iRewrite ("Hpc2" $! v (Next p2')).
   Qed.
 
   Lemma iProto_le_trans p1 p2 p3 :
@@ -652,26 +770,67 @@ Section proto.
     destruct (proto_case p1) as [->|([]&pc1&->)].
     - iRewrite (iProto_le_end_inv with "H"). iApply iProto_le_refl.
     - iDestruct (iProto_le_send_inv with "H") as (a2 pc2) "[Hp2 H]".
-      iRewrite "Hp2"; clear p2. iEval (rewrite /iProto_dual !proto_map_message /=).
+      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 p1') "Hpc". rewrite proto_eq_next_dual'.
-        iMod ("H" with "Hpc") as (p2'') "[H Hpc]".
-        iDestruct ("IH" with "H") as "H". rewrite involutive.
-        iExists (iProto_dual p2''). rewrite proto_eq_next_dual. iFrame.
-      + iIntros (v1 v2 p1' p2') "Hpc1 Hpc2". rewrite !proto_eq_next_dual'.
+      + iIntros (v p1d). iDestruct 1 as (p1') "[Hpc #Hp1d]".
+        iMod ("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).
+        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 ("IH" with "H1") as "H1". iDestruct ("IH" with "H2") as "H2 {IH}".
-        rewrite !involutive /iProto_dual !proto_map_message.
-        iExists _, _, (iProto_dual pt). iFrame. rewrite /= proto_eq_next_dual. iFrame.
+        rewrite !iProto_dual_message' /=. iModIntro. iExists _, _, (iProto_dual pt).
+        iSplitL "H2"; [iNext; by iRewrite "Hp1d"|].
+        iSplitL "H1"; [iNext; 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 !proto_map_message /=).
+      iRewrite "Hp2"; clear p2. iEval (rewrite !iProto_dual_message' /=).
       rewrite iProto_le_unfold; iRight.
       iExists _, _, _, _; do 2 (iSplit; [done|]); simpl.
-      iIntros (v p2') "Hpc". rewrite proto_eq_next_dual'.
-      iMod ("H" with "Hpc") as (p2'') "[H Hpc]".
-      iDestruct ("IH" with "H") as "H". rewrite involutive.
-      iExists (iProto_dual p2''). rewrite proto_eq_next_dual. iFrame.
+      iIntros (v p2d). iDestruct 1 as (p2') "[Hpc #Hp2d]".
+      iMod ("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".
+  Qed.
+
+  Lemma iProto_le_app p1 p2 p3 p4 :
+    iProto_le p1 p2 -∗ iProto_le p3 p4 -∗ iProto_le (p1 <++> p3) (p2 <++> p4).
+  Proof.
+    iIntros "H1 H2". iLöb as "IH" forall (p1 p2 p3 p4).
+    destruct (proto_case p2) as [->|([]&pc2&->)].
+    - iRewrite (iProto_le_end_inv with "H1"). by rewrite !iProto_app_end'.
+    - iDestruct (iProto_le_send_inv with "H1") as (a1 pc1) "[Hp1 H1]".
+      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 "!>".
+        iExists (p1' <++> p3)%proto. iSplitR "Hpc"; [|eauto].
+        iIntros "!>". 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.
+        rewrite -!iProto_app_message' /=. iSplitL "H1".
+        { iIntros "!>". iRewrite "Hp13". iApply ("IH" with "H1").
+          iApply iProto_le_refl. }
+        iSplitL "H2 H1'".
+        { iIntros "!>". 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 "!>".
+      iExists (p2'' <++> p4)%proto. iSplitR "Hpc"; [|eauto].
+      iIntros "!>". iRewrite "Hp13". by iApply ("IH" with "H1").
   Qed.
 
   (** ** Lemmas about the auxiliary definitions and invariants *)
@@ -699,8 +858,8 @@ Section proto.
     iIntros "H● H◯". iDestruct (own_valid_2 with "H● H◯") as "H✓".
     iDestruct (excl_auth_agreeI with "H✓") as "H✓".
     iDestruct (bi.later_eq_1 with "H✓") as "H✓"; iNext.
-    rewrite /iProto_unfold. assert (∀ p,
-      proto_map id iProp_unfold iProp_fold (proto_map id iProp_fold iProp_unfold p) ≡ p) as help.
+    rewrite /iProto_unfold. assert (∀ p, proto_map iProp_unfold iProp_fold
+        (proto_map iProp_fold iProp_unfold p) ≡ p) as help.
     { intros p''. rewrite -proto_map_compose -{2}(proto_map_id p'').
       apply proto_map_ext=> // pc /=; by rewrite iProp_fold_unfold. }
     rewrite -{2}(help p). iRewrite "H✓". by rewrite help.
@@ -734,12 +893,12 @@ Section proto.
       (∃ vl vsl' pc pr',
         ⌜ vsl = vl :: vsl' ⌝ ∗
         iProto_le (proto_message Recv pc) pr ∗
-        pc vl (proto_eq_next pr') ∗
+        pc vl (Next pr') ∗
         iProto_interp vsl' vsr pl pr') ∨
       (∃ vr vsr' pc pl',
         ⌜ vsr = vr :: vsr' ⌝ ∗
         iProto_le (proto_message Recv pc) pl ∗
-        pc vr (proto_eq_next pl') ∗
+        pc vr (Next pl') ∗
         iProto_interp vsl vsr' pl' pr).
   Proof.
     rewrite {1}/iProto_interp. destruct vsl as [|vl vsl]; simpl.
@@ -806,7 +965,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 (proto_eq_next pl') -∗
+    pcl vl (Next pl') -∗
     â–·^(length vsr) iProto_interp (vsl ++ [vl]) vsr pl' pr.
   Proof.
     iIntros "H Hle". iDestruct (iProto_interp_le_l with "H Hle") as "H".
@@ -816,10 +975,10 @@ Section proto.
     - iClear "IH". iDestruct "H" as (p -> ->) "[Hp Hp'] /=".
       iDestruct (iProto_le_dual with "Hp") as "Hp".
       iDestruct (iProto_le_trans with "Hp Hp'") as "Hp".
-      rewrite /iProto_dual proto_map_message /=.
+      rewrite iProto_dual_message' /=.
       iApply iProto_interp_unfold. iRight; iLeft.
       iExists vl, [], _, (iProto_dual pl'). iSplit; [done|]. iFrame "Hp"; simpl.
-      rewrite proto_eq_next_dual. iFrame "Hpcl". iApply iProto_interp_nil.
+      iSplitL; [by auto|]. iApply iProto_interp_nil.
     - iDestruct "H" as (vl' vsl' pc' pr' ->) "(Hpr & Hpc' & H)".
       iDestruct ("IH" with "[%] [//] H Hpcl") as "H"; [simpl; lia|].
       iNext. iApply (iProto_interp_le_r with "[-Hpr] Hpr"); clear pr.
@@ -829,7 +988,7 @@ 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' (proto_eq_next pl'')) in "Hpcl'"; clear pc'.
+      iRewrite ("Hpc" $! vr' (Next pl'')) in "Hpcl'"; clear pc'.
       iMod ("Hle" with "Hpcl' Hpcl")
         as (pc1 pc2 pt) "(Hpl'' & Hpl' & Hpc1 & Hpc2)".
       iNext. iDestruct (iProto_interp_le_l with "H Hpl''") as "H".
@@ -841,7 +1000,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 (proto_eq_next pr) ∗ ▷ iProto_interp vsl vsr pl pr.
+    ◇ ∃ pr, pcr vl (Next 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.
@@ -852,7 +1011,7 @@ Section proto.
       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' (proto_eq_next pr')). }
+      { by iRewrite -("Hpc" $! vl' (Next pr')). }
       iModIntro. iExists pr''. iFrame "Hpr".
       by iApply (iProto_interp_le_r with "Hinterp").
     - iDestruct "H" as (vr vsr' pc' pl'' ->) "(Hpl & Hpc' & Hinterp)".
diff --git a/theories/channel/proto_model.v b/theories/channel/proto_model.v
index 4329ef3..b905a74 100644
--- a/theories/channel/proto_model.v
+++ b/theories/channel/proto_model.v
@@ -35,7 +35,7 @@ The defined functions on the type [proto] are:
   all terminations [END] in [p1] with [p2]. *)
 From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import cofe_solver.
+From actris.utils Require Import cofe_solver_2.
 Set Default Proof Using "Type".
 
 Module Export action.
@@ -48,34 +48,36 @@ Module Export action.
   Canonical Structure actionO := leibnizO action.
 End action.
 
-Definition protoOF_helper (V : Type) (PROPn PROP : ofeT) : oFunctor :=
-  optionOF (actionO * (V -d> (▶ ∙ -n> PROPn) -n> PROP)).
-Definition proto_result (V : Type) (PROPn PROP : ofeT) `{!Cofe PROPn, !Cofe PROP} :
-  solution (protoOF_helper V PROPn PROP) := solver.result _.
+Definition proto_auxO (V : Type) (PROP : ofeT) (A : ofeT) : ofeT :=
+  optionO (prodO actionO (V -d> laterO A -n> PROP)).
+Definition proto_auxOF (V : Type) (PROP : ofeT) : oFunctor :=
+  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 :=
-  proto_result V PROPn PROP.
+  proto_result V PROPn _ PROP _.
 Instance proto_cofe {V} `{!Cofe PROPn, !Cofe PROP} : Cofe (proto V PROPn PROP).
 Proof. apply _. Qed.
+Lemma proto_iso {V} `{!Cofe PROPn, !Cofe PROP} :
+  ofe_iso (proto_auxO V PROP (proto V PROP PROPn)) (proto V PROPn PROP).
+Proof. apply proto_result. Qed.
 
 Definition proto_fold {V} `{!Cofe PROPn, !Cofe PROP} :
-    protoOF_helper V PROPn PROP (proto V PROPn PROP) _ -n> proto V PROPn PROP :=
-  solution_fold (proto_result V PROPn PROP).
+  proto_auxO V PROP (proto V PROP PROPn) -n> proto V PROPn PROP := ofe_iso_1 proto_iso.
 Definition proto_unfold {V} `{!Cofe PROPn, !Cofe PROP} :
-    proto V PROPn PROP -n> protoOF_helper V PROPn PROP (proto V PROPn PROP) _ :=
-  solution_unfold (proto_result V PROPn PROP).
-
+  proto V PROPn PROP -n> proto_auxO V PROP (proto V PROP PROPn) := ofe_iso_2 proto_iso.
 Lemma proto_fold_unfold {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
   proto_fold (proto_unfold p) ≡ p.
-Proof. apply solution_fold_unfold. Qed.
+Proof. apply (ofe_iso_12 proto_iso). Qed.
 Lemma proto_unfold_fold {V} `{!Cofe PROPn, !Cofe PROP}
-    (p : protoOF_helper V PROPn PROP (proto V PROPn PROP) _) :
+    (p : proto_auxO V PROP (proto V PROP PROPn)) :
   proto_unfold (proto_fold p) ≡ p.
-Proof. apply solution_unfold_fold. Qed.
+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 PROPn PROP) -n> PROPn) -n> PROP) : proto V PROPn PROP :=
+    (pc : V → laterO (proto V PROP PROPn) -n> PROP) : proto V PROPn PROP :=
   proto_fold (Some (a, pc)).
 
 Instance proto_message_ne {V} `{!Cofe PROPn, !Cofe PROP} a n :
@@ -99,7 +101,7 @@ Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
 
 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 pc', pc1 v pc' ≡ pc2 v pc').
+  ⊣⊢@{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.
@@ -120,217 +122,140 @@ 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.
 
-Definition proto_cont_map
-   `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP', !Cofe A, !Cofe B}
-    (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') (h : A -n> B) :
-    ((laterO A -n> PROPn) -n> PROP) -n> (laterO B -n> PROPn') -n> PROP' :=
-  ofe_morO_map (ofe_morO_map (laterO_map h) gn) g.
-
-(** Append *)
-Program Definition proto_app_flipped_aux {V} `{!Cofe PROPn, !Cofe PROP}
-    (p2 : proto V PROPn PROP) (rec : proto V PROPn PROP -n> proto V PROPn PROP) :
-    proto V PROPn PROP -n> proto V PROPn PROP := λne p1,
-  match proto_unfold p1 return _ with
-  | None => p2
-  | Some (a, c) => proto_message a (proto_cont_map cid cid rec ∘ c)
-  end.
-Next Obligation.
-  intros V PROPn ? PROP ? rec n p2 p1 p1' Hp.
-  apply (ofe_mor_ne _ _ proto_unfold) in Hp.
-  destruct Hp as [[??][??] [-> ?]|]; simplify_eq/=; last done.
-  f_equiv=> v /=. by f_equiv.
-Qed.
-
-Instance proto_app_flipped_aux_contractive {V} `{!Cofe PROPn, !Cofe PROP}
-  (p2 : proto V PROPn PROP) : Contractive (proto_app_flipped_aux p2).
-Proof.
-  intros n rec1 rec2 Hrec p1. simpl.
-  destruct (proto_unfold p1) as [[a c]|]; last done.
-  f_equiv=> v /=. do 2 f_equiv.
-  intros=> p'. apply Next_contractive. destruct n as [|n]=> //=.
-Qed.
-
-Definition proto_app_flipped {V} `{!Cofe PROPn, !Cofe PROP}
-    (p2 : proto V PROPn PROP) : proto V PROPn PROP -n> proto V PROPn PROP :=
-  fixpoint (proto_app_flipped_aux p2).
-Definition proto_app {V} `{!Cofe PROPn, !Cofe PROP}
-  (p1 p2 : proto V PROPn PROP) : proto V PROPn PROP := proto_app_flipped p2 p1.
-Instance: Params (@proto_app) 5 := {}.
-
-Lemma proto_app_flipped_unfold {V} `{!Cofe PROPn, !Cofe PROP} (p1 p2 : proto V PROPn PROP):
-  proto_app_flipped p2 p1 ≡ proto_app_flipped_aux p2 (proto_app_flipped p2) p1.
-Proof. apply (fixpoint_unfold (proto_app_flipped_aux p2)). Qed.
-Lemma proto_app_unfold {V} `{!Cofe PROPn, !Cofe PROP} (p1 p2 : proto V PROPn PROP):
-  proto_app (V:=V) p1 p2 ≡ proto_app_flipped_aux p2 (proto_app_flipped p2) p1.
-Proof. apply (fixpoint_unfold (proto_app_flipped_aux p2)). Qed.
-
-Lemma proto_app_end_l {V} `{!Cofe PROPn, !Cofe PROP} (p2 : proto V PROPn PROP) :
-  proto_app proto_end p2 ≡ p2.
-Proof.
-  rewrite proto_app_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; rewrite E; inversion Hfold.
-Qed.
-Lemma proto_app_message {V} `{!Cofe PROPn, !Cofe PROP} a c (p2 : proto V PROPn PROP) :
-  proto_app (proto_message a c) p2
-  ≡ proto_message a (proto_cont_map cid cid (proto_app_flipped p2) ∘ c).
-Proof.
-  rewrite proto_app_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.
-Qed.
-
-Instance proto_app_ne {V} `{!Cofe PROPn, !Cofe PROP} :
-  NonExpansive2 (proto_app (V:=V) (PROPn:=PROPn) (PROP:=PROP)).
-Proof.
-  intros n p1 p1' Hp1 p2 p2' Hp2. rewrite /proto_app -Hp1 {p1' Hp1}.
-  revert p1. induction (lt_wf n) as [n _ IH]=> p1 /=.
-  rewrite !proto_app_flipped_unfold /proto_app_flipped_aux /=.
-  destruct (proto_unfold p1) as [[a c]|]; last done.
-  f_equiv=> v f /=. do 2 f_equiv. intros p. apply Next_contractive.
-  destruct n as [|n]=> //=. apply IH; first lia; auto using dist_S.
-Qed.
-Instance proto_app_proper {V} `{!Cofe PROPn, !Cofe PROP} :
-  Proper ((≡) ==> (≡) ==> (≡)) (proto_app (V:=V) (PROPn:=PROPn) (PROP:=PROP)).
-Proof. apply (ne_proper_2 _). Qed.
-
-Lemma proto_app_end_r {V} `{!Cofe PROPn, !Cofe PROP} (p1 : proto V PROPn PROP) :
-  proto_app p1 proto_end ≡ p1.
-Proof.
-  apply equiv_dist=> n. revert p1. induction (lt_wf n) as [n _ IH]=> p1 /=.
-  destruct (proto_case p1) as [->|(a & c & ->)].
-  - by rewrite !proto_app_end_l.
-  - rewrite !proto_app_message /=. f_equiv=> v c' /=. f_equiv=> p' /=. f_equiv.
-    apply Next_contractive. destruct n as [|n]=> //=.
-    apply IH; first lia; auto using dist_S.
-Qed.
-Lemma proto_app_assoc {V} `{!Cofe PROPn, !Cofe PROP} (p1 p2 p3 : proto V PROPn PROP) :
-  proto_app p1 (proto_app p2 p3) ≡ proto_app (proto_app p1 p2) p3.
-Proof.
-  apply equiv_dist=> n. revert p1. induction (lt_wf n) as [n _ IH]=> p1 /=.
-  destruct (proto_case p1) as [->|(a & c & ->)].
-  - by rewrite !proto_app_end_l.
-  - rewrite !proto_app_message /=. f_equiv=> v c' /=. f_equiv=> p' /=. f_equiv.
-    apply Next_contractive. destruct n as [|n]=> //=.
-    apply IH; first lia; auto using dist_S.
-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.
+
 Program Definition proto_map_aux {V}
    `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
-    (f : action → action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP')
-    (rec : proto V PROPn PROP -n> proto V PROPn' 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 (f a) (proto_cont_map gn g rec ∘ c)
+  | Some (a, c) => proto_message a (proto_cont_map g rec ∘ c)
   end.
 Next Obligation.
-  intros V PROPn ? PROPn' ? PROP ? PROP' ? f g1 g2 rec n p1 p2 Hp.
+  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.
 Qed.
 Instance proto_map_aux_contractive {V}
-   `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
-    (f : action → action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
-  Contractive (proto_map_aux (V:=V) f gn g).
+   `{!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 /=. do 2 f_equiv.
-  intros=> p'. apply Next_contractive. destruct n as [|n]=> //=.
+  f_equiv=> v p' /=. do 2 f_equiv. apply Next_contractive.
+  destruct n as [|n]=> //=.
 Qed.
+
+Definition proto_map_aux_2 {V}
+   `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
+    (gn : PROPn' -n> PROPn) (g : PROP -n> PROP')
+    (rec : proto V PROPn PROP -n> proto V PROPn' PROP') :
+    proto V PROPn PROP -n> proto V PROPn' PROP' :=
+  proto_map_aux g (proto_map_aux gn rec).
+Instance proto_map_aux_2_contractive {V}
+   `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
+    (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
+  Contractive (proto_map_aux_2 (V:=V) gn g).
+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'}
-    (f : action → action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
+    (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
     proto V PROPn PROP -n> proto V PROPn' PROP' :=
-  fixpoint (proto_map_aux f gn g).
+  fixpoint (proto_map_aux_2 gn g).
 
-Lemma proto_map_unfold {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
-    (f : action → action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') p :
-  proto_map (V:=V) f gn g p ≡ proto_map_aux f gn g (proto_map f gn g) p.
-Proof. apply (fixpoint_unfold (proto_map_aux f gn g)). Qed.
+Lemma proto_map_unfold {V}
+    `{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hc:!Cofe PROP, Hc':!Cofe PROP'}
+    (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') p :
+  proto_map (V:=V) gn g p ≡ proto_map_aux g (proto_map g gn) p.
+Proof.
+  apply equiv_dist=> n. revert PROPn Hcn PROPn' Hcn' PROP Hc PROP' Hc' gn g p.
+  induction (lt_wf n) as [n _ IH]=>
+    PROPn Hcn PROPn' Hcn' PROP Hc PROP' Hc' gn g p.
+  etrans; [apply equiv_dist, (fixpoint_unfold (proto_map_aux_2 gn g))|].
+  apply proto_map_aux_contractive; destruct n as [|n]; [done|]; simpl.
+  symmetry. apply: IH. lia.
+Qed.
 Lemma proto_map_end {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
-    (f : action → action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
-  proto_map (V:=V) f gn g proto_end ≡ proto_end.
+    (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; rewrite E; inversion Hfold.
+  by destruct (proto_unfold (proto_fold None)) as [[??]|] eqn:E; inversion Hfold.
 Qed.
 Lemma proto_map_message {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
-    (f : action → action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') a c :
-  proto_map (V:=V) f gn g (proto_message a c) ≡ proto_message (f a) (proto_cont_map gn g (proto_map f gn g) ∘ c).
+    (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).
 Proof.
   rewrite proto_map_unfold /proto_message /=.
-  pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn) (PROP:=PROP) (Some (a, c))) as Hfold.
+  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.
 Qed.
 
-Lemma proto_map_ne {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
-    (f1 f2 : action → action) (gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p n :
-  (∀ a, f1 a = f2 a) → (∀ x, gn1 x ≡{n}≡ gn2 x) → (∀ x, g1 x ≡{n}≡ g2 x) →
-  proto_map (V:=V) f1 gn1 g1 p ≡{n}≡ proto_map (V:=V) f2 gn2 g2 p.
+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) →
+  proto_map (V:=V) gn1 g1 p ≡{n}≡ proto_map (V:=V) gn2 g2 p.
 Proof.
-  intros Hf. revert p. induction (lt_wf n) as [n _ IH]=> p Hgn Hg /=.
+  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 /= Hf. f_equiv=> v /=. do 2 (f_equiv; last done).
+  - 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.
 Qed.
 Lemma proto_map_ext {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
-    (f1 f2 : action → action) (gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p :
-  (∀ a, f1 a = f2 a) → (∀ x, gn1 x ≡ gn2 x) → (∀ x, g1 x ≡ g2 x) →
-  proto_map (V:=V) f1 gn1 g1 p ≡ proto_map (V:=V) f2 gn2 g2 p.
+    (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.
 Proof.
-  intros Hf Hgn Hg. apply equiv_dist=> n.
+  intros Hgn Hg. apply equiv_dist=> n.
   apply proto_map_ne=> // ?; by apply equiv_dist.
 Qed.
-Lemma proto_map_id {V} `{!Cofe PROPn, !Cofe PROP} (p : proto V PROPn PROP) :
-  proto_map id cid cid p ≡ p.
+Lemma proto_map_id {V} `{Hcn:!Cofe PROPn, Hc:!Cofe PROP} (p : proto V PROPn PROP) :
+  proto_map cid cid p ≡ p.
 Proof.
-  apply equiv_dist=> n. revert p. induction (lt_wf n) as [n _ IH]=> p /=.
+  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=> p' /=. f_equiv.
+  - 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.
 Qed.
 Lemma proto_map_compose {V}
-   `{!Cofe PROPn, !Cofe PROPn', !Cofe PROPn'', !Cofe PROP, !Cofe PROP', !Cofe PROP''}
-    (f1 f2 : action → action)
+   `{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hcn'':!Cofe PROPn'',
+     Hc:!Cofe PROP, Hc':!Cofe PROP', Hc'':!Cofe PROP''}
     (gn1 : PROPn'' -n> PROPn') (gn2 : PROPn' -n> PROPn)
     (g1 : PROP -n> PROP') (g2 : PROP' -n> PROP'') (p : proto V PROPn PROP) :
-  proto_map (f2 ∘ f1) (gn2 ◎ gn1) (g2 ◎ g1) p ≡ proto_map f2 gn1 g2 (proto_map f1 gn2 g1 p).
+  proto_map (gn2 ◎ gn1) (g2 ◎ g1) p ≡ proto_map gn1 g2 (proto_map gn2 g1 p).
 Proof.
-  apply equiv_dist=> n. revert p. induction (lt_wf n) as [n _ IH]=> p /=.
+  apply equiv_dist=> n. revert PROPn Hcn PROPn' Hcn' PROPn'' Hcn''
+    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. move=> p' /=.
-    do 3 f_equiv. apply Next_contractive. destruct n as [|n]=> //=.
-    apply IH; first lia; auto using dist_S.
-Qed.
-
-Lemma proto_map_app {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
-    (f : action → action) (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') p1 p2 :
-  proto_map (V:=V) f gn g (proto_app p1 p2)
-  ≡ proto_app (proto_map (V:=V) f gn g p1) (proto_map (V:=V) f gn g p2).
-Proof.
-  apply equiv_dist=> n. revert p1 p2. induction (lt_wf n) as [n _ IH]=> p1 p2 /=.
-  destruct (proto_case p1) as [->|(a & c & ->)].
-  - by rewrite proto_map_end !proto_app_end_l.
-  - rewrite proto_map_message !proto_app_message proto_map_message /=.
-    f_equiv=> v c' /=. do 2 f_equiv. move=> p' /=. do 2 f_equiv.
+  - 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.
 Qed.
@@ -340,7 +265,7 @@ Program Definition protoOF (V : Type) (Fn F : oFunctor)
     `{!∀ A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F A B)} : oFunctor := {|
   oFunctor_car A _ B _ := proto V (oFunctor_car Fn B A) (oFunctor_car F A B);
   oFunctor_map A1 _ A2 _ B1 _ B2 _ fg :=
-    proto_map id (oFunctor_map Fn (fg.2, fg.1)) (oFunctor_map F fg)
+    proto_map (oFunctor_map Fn (fg.2, fg.1)) (oFunctor_map F fg)
 |}.
 Next Obligation.
   intros V Fn F ?? A1 ? A2 ? B1 ? B2 ? n f g [??] p; simpl in *.
@@ -353,7 +278,7 @@ Qed.
 Next Obligation.
   intros V Fn F ?? A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' p; simpl in *.
   rewrite -proto_map_compose.
-  apply proto_map_ext=> //= y; by rewrite oFunctor_compose.
+  apply proto_map_ext=> //= y; by rewrite ofe.oFunctor_compose.
 Qed.
 
 Instance protoOF_contractive (V : Type) (Fn F : oFunctor)
-- 
GitLab