diff --git a/multris/channel/proto_model.v b/multris/channel/proto_model.v
index f95afa26e7b6b72fe9b900f74050db33885a1ca9..44551fae434d8a47f196ff1174035b502435eae3 100644
--- a/multris/channel/proto_model.v
+++ b/multris/channel/proto_model.v
@@ -34,6 +34,7 @@ The defined functions on the type [proto] are:
   a given protocol.
 - [proto_app], which appends two protocols [p1] and [p2], by substituting
   all terminations [END] in [p1] with [p2]. *)
+From stdpp Require Import gmap.
 From iris.algebra Require Import gmap.
 From iris.base_logic Require Import base_logic.
 From iris.proofmode Require Import proofmode.
@@ -62,187 +63,154 @@ Module Export action.
   Proof. by intros [[]]. Qed.
 End action.
 
+Notation proto_aux V PROP A :=
+  (gmap action (V -d> laterO A -n> PROP)).
 Notation proto_auxO V PROP A :=
-  (gmapO actionO (V -d> later A -n> PROP)).
-(* Notation proto_auxOF V PROP := *)
-(*   (gmapOF actionO ((V -d> ▶ ∙ -n> PROP))). *)
-(* Definition proto_auxO (V : Type) (PROP : ofe) (A : ofe) : ofe := *)
-(*   (gmapO actionO (V -d> laterO A -n> PROP)). *)
-Definition proto_auxOF (V : Type) (PROP : ofe) : oFunctor :=
+  (gmapO actionO (V -d> laterO A -n> PROP)).
+Definition proto_auxOF V PROP :=
   (gmapOF actionO ((V -d> ▶ ∙ -n> PROP))).
 
 Definition proto_result (V : Type) := result_2 (proto_auxOF V).
-Definition proto (V : Type) (PROPn PROP : ofe) `{!Cofe PROPn, !Cofe PROP} : ofe :=
+Definition pre_protoO (V : Type) (PROPn PROP : ofe) `{!Cofe PROPn, !Cofe PROP} : ofe :=
   solution_2_car (proto_result V) PROPn _ PROP _.
+Global Instance pre_proto_cofe {V} `{!Cofe PROPn, !Cofe PROP} : Cofe (pre_protoO V PROPn PROP).
+Proof. apply _. Qed.
+
+Definition protoO (V : Type) (PROPn PROP : ofe) `{!Cofe PROPn, !Cofe PROP} : ofe :=
+  proto_auxO V PROP (pre_protoO V PROP PROPn).
+Global Instance protoO_cofe {V} `{!Cofe PROPn, !Cofe PROP} : Cofe (protoO V PROPn PROP).
+Proof. apply _. Qed.
+Lemma protoO_iso {V} `{!Cofe PROPn, !Cofe PROP} :
+  ofe_iso (protoO V PROPn PROP) (pre_protoO V PROPn PROP).
+Proof. apply proto_result. Qed.
+
+Definition proto (V : Type) (PROPn PROP : ofe) `{!Cofe PROPn, !Cofe PROP} : ofe :=
+  proto_aux V PROP (pre_protoO V PROP PROPn).
 Global 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).
+  ofe_iso (proto V PROPn PROP) (pre_protoO V PROPn PROP).
 Proof. apply proto_result. Qed.
 
-Definition proto_fold {V} `{!Cofe PROPn, !Cofe 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> proto_auxO V PROP (proto V PROP PROPn) := ofe_iso_2 proto_iso.
+  proto V PROPn PROP -n> pre_protoO V PROPn PROP := ofe_iso_1 proto_iso.
+Definition proto_fold {V} `{!Cofe PROPn, !Cofe PROP} :
+  pre_protoO V PROPn PROP -n> proto V PROPn PROP := 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 (ofe_iso_12 proto_iso). Qed.
+Proof. apply (ofe_iso_21 proto_iso). Qed.
 Lemma proto_unfold_fold {V} `{!Cofe PROPn, !Cofe PROP}
-    (p : proto_auxO V PROP (proto V PROP PROPn)) :
+    (p : pre_protoO V PROP PROPn) :
   proto_unfold (proto_fold p) ≡ p.
-Proof. apply (ofe_iso_21 proto_iso). Qed.
-
-(* Derived laws *)
-Section internal_eq_derived.
-  Context {PROP : bi} `{!BiInternalEq PROP}.
-  Context `{Countable K} {A : ofe}.
-  Implicit Types P : PROP.
-
-  (* Force implicit argument PROP *)
-  Notation "P ⊢ Q" := (P ⊢@{PROP} Q).
-  Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
-
-  Lemma gmap_equivI (m1 m2 : gmap K A) :
-    m1 ≡ m2 ⊣⊢ ∀ i, m1 !! i ≡ m2 !! i.
-  Proof. Admitted.
-
-  Lemma gmap_union_equiv_eqI (m m1 m2 : gmap K A) :
-    m ≡ m1 ∪ m2 ⊣⊢ ∃ m1' m2', ⌜ m = m1' ∪ m2' ⌝ ∧ m1' ≡ m1 ∧ m2' ≡ m2.
-  Proof. Admitted.
-
-  Lemma gmap_singleton_equivI (k1 k2 : K) (a1 a2 : A) :
-    {[ k1 := a1 ]} ≡ {[ k2 := a2 ]} ⊣⊢ ⌜ k1 = k2 ⌝ ∧ a1 ≡ a2.
-  Proof. Admitted.
-
-End internal_eq_derived.
+Proof. apply (ofe_iso_12 proto_iso). Qed.
 
-Global Instance subseteq_proper `{Countable K} {A:Type} `{Equiv A} :
-  Proper ((≡@{gmap K A}) ==> (≡@{gmap K A}) ==> iff) (⊆).
-Proof. Admitted.
-Global Instance subset_proper `{Countable K} {A:Type} `{Equiv A} :
-  Proper ((≡@{gmap K A}) ==> (≡@{gmap K A}) ==> iff) (⊂).
-Proof. solve_proper. Qed.
-  
-Definition proto_end {V} `{!Cofe PROPn, !Cofe PROP} : proto V PROPn PROP :=
-  proto_fold ∅ .
+Definition proto_end {V} `{!Cofe PROPn, !Cofe PROP} : proto V PROPn PROP := ∅ .
 Definition proto_message {V} `{!Cofe PROPn, !Cofe PROP} (a : action)
-    (m : V → laterO (proto V PROP PROPn) -n> PROP) : proto V PROPn PROP :=
-  proto_fold {[a := m]}.
+  (m : V -d> later (proto V PROP PROPn) -n> PROP) : proto V PROPn PROP :=
+  ({[a := (λ v, m v ◎ laterO_map proto_fold)]}).
 Definition proto_union {V} `{!Cofe PROPn, !Cofe PROP} (p1 p2 : proto V PROPn PROP) : proto V PROPn PROP :=
-  proto_fold (((proto_unfold p1):gmap _ _) ∪ (proto_unfold p2)).
+  (p1:gmap _ _) ∪ p2.
 
 Global 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 apply insert_ne.
+  intros c1 c2 Hc. rewrite /proto_message.
+  apply insert_ne; [|done]. solve_proper.
 Qed.
 
-(* TODO: Why does unification algorithm fail here? *)
 Global Instance proto_message_proper {V} `{!Cofe PROPn, !Cofe PROP} a :
   Proper (pointwise_relation V (≡) ==> (≡))
          (proto_message (PROPn:=PROPn) (PROP:=PROP) a).
-Proof. intros c1 c2 Hc. rewrite /proto_message. f_equiv. by apply: insert_proper. Qed.
+Proof. intros c1 c2 Hc. rewrite /proto_message. apply: insert_proper; [|done]. solve_proper.
+Qed.
 
 Global Instance proto_union_ne {V} `{!Cofe PROPn, !Cofe PROP} n :
   Proper ((dist n) ==> (dist n) ==> dist n)
          (proto_union (V:=V) (PROPn:=PROPn) (PROP:=PROP)).
 Proof.
-  intros p11 p12 Hp1 p21 p22 Hp2. rewrite /proto_union. by do 3 f_equiv.
+  intros p11 p12 Hp1 p21 p22 Hp2. rewrite /proto_union. by f_equiv.
 Qed.
 
+(* TODO: Why does unification algorithm fail here? *)
 Global Instance proto_union_proper {V} `{!Cofe PROPn, !Cofe PROP} :
   Proper ((≡) ==> (≡) ==> (≡))
          (proto_union (V:=V) (PROPn:=PROPn) (PROP:=PROP)).
-Proof. intros p11 p12 Hp1 p21 p22 Hp2. rewrite /proto_union. solve_proper. Qed.
+Proof.
+  intros p11 p12 Hp1 p21 p22 Hp2. rewrite /proto_union. by f_equiv.
+Qed.
 
-(* TODO: Missing Proper stuff *)
+(* Should hold in the same way map_ind holds *)
 Lemma proto_ind {V} `{!Cofe PROPn, !Cofe PROP} (P : proto V PROPn PROP → Prop) :
   Proper ((≡) ==> impl) P →
-  P proto_end → (∀ i x p, proto_unfold p !! i ≡ None → P p → P (proto_union (proto_message i x) p)) → ∀ m, P m.
+  P proto_end → (∀ i x p, p !! i ≡ None → P p → P (proto_union (proto_message i x) p)) → ∀ m, P m.
 Proof.
-  intros HP ? Hins m'.
-  assert (∃ m, m = proto_unfold m') as [m Hm].
-  { eexists _. done. }
-  revert Hm. revert m'.
+  intros HP ? Hins m.
   induction (map_wf m) as [m _ IH].
-  intros m' Hm.
   destruct (map_choose_or_empty m) as [(i&x&?)| H'].
   {
-    assert (m' ≡ proto_union (proto_message i x) (proto_fold (delete i (proto_unfold m'))))
-      as Heq.
+    assert (m ≡ proto_union (proto_message i (λ v, x v ◎ laterO_map proto_unfold)) (delete i m)) as Heq.
     {
-      rewrite -Hm /proto_union /proto_message !proto_unfold_fold -(proto_fold_unfold m').
-      f_equiv. rewrite -Hm -insert_union_singleton_l. by rewrite insert_delete.
-    }
+      rewrite /proto_message /proto_union.
+      rewrite -insert_union_singleton_l.
+      intros i'.
+      (* TODO: Simplify *)
+      destruct (decide (i=i')) as [->|].
+      { rewrite H0. rewrite lookup_insert. f_equiv.
+        intros v.
+        intros x''.
+        simpl.
+        rewrite -later_map_compose.
+        simpl. f_equiv.
+        destruct x''.
+        rewrite later_map_Next. f_equiv.
+        simpl. rewrite proto_unfold_fold. done. }
+      rewrite lookup_insert_ne; [|done].
+      by rewrite lookup_delete_ne. }
     rewrite Heq.
     apply Hins.
-    { rewrite -Hm lookup_proper; [|apply proto_unfold_fold]. by rewrite lookup_delete. }
-    eapply IH; [|done]. rewrite -Hm (proto_unfold_fold (delete i m)).
-    by apply: delete_subset.
+    { by rewrite lookup_delete. }
+    eapply IH. by apply: delete_subset.
   }
   rewrite /proto_end in H.
-  rewrite Hm in H'. rewrite -H' in H. by rewrite -(proto_fold_unfold m').
+  by rewrite -H' in H.
 Qed.
-
+  
 Global Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
   Inhabited (proto V PROPn PROP) := populate proto_end.
 
 Lemma proto_message_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a1 a2 m1 m2 :
   proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a1 m1 ≡ proto_message a2 m2
   ⊣⊢@{SPROP} ⌜ a1 = a2 ⌝ ∧ (∀ v p', m1 v p' ≡ m2 v p').
-Proof.
-  trans (proto_unfold (proto_message a1 m1) ≡ proto_unfold (proto_message a2 m2) : SPROP)%I.
-  { iSplit.
-    - iIntros "Heq". by iRewrite "Heq".
-    - iIntros "Heq". rewrite -{2}(proto_fold_unfold (proto_message _ _)).
-      iRewrite "Heq". by rewrite proto_fold_unfold. }
-  rewrite /proto_message !proto_unfold_fold.
-  
-  rewrite gmap_singleton_equivI /=.
-  rewrite discrete_fun_equivI.
-  by setoid_rewrite ofe_morO_equivI.
-Qed.
-
+Proof. Admitted.
 Lemma proto_message_end_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a m :
   proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a m ≡ proto_end ⊢@{SPROP} False.
-Proof.
-  trans (proto_unfold (proto_message a m) ≡ proto_unfold proto_end : SPROP)%I.
-  { iIntros "Heq". by iRewrite "Heq". }
-  rewrite /proto_message !proto_unfold_fold.
-Admitted.
+Proof. Admitted.
 Lemma proto_end_message_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a m :
   proto_end ≡ proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a m ⊢@{SPROP} False.
 Proof. by rewrite internal_eq_sym proto_message_end_equivI. 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,
-  (* fmap (λ (m:proto V PROPn PROP), (λ v, g ◎ m v ◎ laterO_map rec)) (proto_unfold p). *)
-  (* proto_fold $ gmap_fmap _ _ (λ m, (λ v, g ◎ m v ◎ laterO_map rec)) (proto_unfold p). *)
-  proto_fold $ fmap (λ m, (λ v, g ◎ m v ◎ laterO_map rec)) (proto_unfold p).
+  proto V PROPn PROP -n> proto V PROPn' PROP' := λne p,
+    (λ m, λ v, g ◎ m v ◎ laterO_map proto_unfold ◎ laterO_map rec ◎ laterO_map proto_fold) <$> p.
 Next Obligation.
   intros V PROPn ? PROPn' ? PROP ? PROP' ? g rec n p1 p2 Hp.
-  f_equiv. simpl.
-  apply (_ : NonExpansive proto_unfold) in Hp.
-Admitted.
-(* TODO: Needs non expansiveness of fmap *)
-(* (* Admitted. *) *)
-(*   apply map_fmap_ne. *)
-(*   apply gmap_fmap_ne_ext. *)
-(*   apply proto_elim_ne=> // a m1 m2 Hm. by repeat f_equiv. *)
-(* Qed. *)
+  apply: (map_fmap_ne _ n _ p1 p2); [|done].
+  solve_proper.
+Qed.
 
 Global 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. Admitted.
-(*   intros n rec1 rec2 Hrec p. simpl. apply proto_elim_ne=> // a m1 m2 Hm. *)
-(*   f_equiv=> v p' /=. do 2 f_equiv; [done|]. *)
-(*   apply Next_contractive; by dist_later_intro as n' Hn'. *)
-(* Qed. *)
+Proof.
+  intros n p1 p2 Hp. rewrite /proto_map_aux.
+  intros p. simpl.
+  apply: gmap_fmap_ne_ext.
+  intros i x Hix v. f_equiv. f_equiv. f_contractive.
+  done.
+Qed.
 
 Definition proto_map_aux_2 {V}
    `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
@@ -280,28 +248,37 @@ Lemma proto_map_end {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
   proto_map (V:=V) gn g proto_end ≡ proto_end.
 Proof.
   rewrite proto_map_unfold /proto_map_aux /=.
-  (* pose proof (proto_unfold_fold (V:=V) (PROPn:=PROPn) (PROP:=PROP) ∅) as Hfold. *)
-  rewrite /proto_end. f_equiv.
-  rewrite -(fmap_empty (λ (m : V → laterO (proto V PROP PROPn) -n> PROP) (v : V),
-                g â—Ž m v â—Ž laterO_map (proto_map g gn))).
-  f_equiv.
-  (* proto_unfold_fold not working ??? *)
-Admitted.
+  done.
+Qed.
 Lemma proto_map_message {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
     (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') a m :
   proto_map (V:=V) gn g (proto_message a m)
   ≡ proto_message a (λ v, g ◎ m v ◎ laterO_map (proto_map g gn)).
 Proof.
   rewrite proto_map_unfold /proto_map_aux /=.
-  rewrite /proto_message. f_equiv.
-Admitted.
+  rewrite /proto_message.
+  rewrite fmap_insert. rewrite fmap_empty.
+  intros a'. destruct (decide (a=a')).
+  { subst. rewrite !lookup_insert.
+    f_equiv.
+    intros v. f_equiv. f_equiv.
+    intros x. simpl. f_equiv. f_equiv.
+    intros y. simpl. rewrite proto_fold_unfold. done.
+  }
+  by rewrite !lookup_insert_ne.
+Qed.
 Lemma proto_map_union {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
     (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') p1 p2 :
   proto_map (V:=V) gn g (proto_union p1 p2)
   ≡ proto_union (proto_map gn g p1) (proto_map gn g p2).
 Proof.
   rewrite proto_map_unfold /proto_map_aux /=.
-Admitted.
+  rewrite proto_map_unfold /proto_map_aux /=.
+  rewrite proto_map_unfold /proto_map_aux /=.
+  rewrite !/proto_union.
+  rewrite !map_fmap_union.
+  f_equiv.
+Qed.
 
 Lemma proto_map_ne {V}
     `{Hcn:!Cofe PROPn, Hcn':!Cofe PROPn', Hc:!Cofe PROP, Hc':!Cofe PROP'}
@@ -350,7 +327,7 @@ Lemma proto_map_compose {V}
     (gn1 : PROPn'' -n> PROPn') (gn2 : PROPn' -n> PROPn)
     (g1 : PROP -n> PROP') (g2 : PROP' -n> PROP'') (p : proto V PROPn PROP) :
   proto_map (gn2 ◎ gn1) (g2 ◎ g1) p ≡ proto_map gn1 g2 (proto_map gn2 g1 p).
-Proof.
+Proof.  
   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'' ?
@@ -389,7 +366,7 @@ Qed.
 Global Instance protoOF_contractive (V : Type) (Fn F : oFunctor)
     `{!∀ A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car Fn A B)}
     `{!∀ A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F A B)} :
-  oFunctorContractive Fn → oFunctorContractive F →
+  oFunctorContractive Fn → oFunctorContractive F → 
   oFunctorContractive (protoOF V Fn F).
 Proof.
   intros HFn HF A1 ? A2 ? B1 ? B2 ? n f g Hfg p; simpl in *.