diff --git a/multris/channel/proto_model.v b/multris/channel/proto_model.v
index 44551fae434d8a47f196ff1174035b502435eae3..71bc2e04b2638d42212686a460c956db448216a3 100644
--- a/multris/channel/proto_model.v
+++ b/multris/channel/proto_model.v
@@ -34,11 +34,12 @@ 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.base_logic.lib Require Import iprop.
 From iris.proofmode Require Import proofmode.
 From multris.utils Require Import cofe_solver_2.
+
 Set Default Proof Using "Type".
 
 Module Export action.
@@ -179,15 +180,40 @@ 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 :
+Lemma proto_message_equivI {Σ} `{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. 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. 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.
+  ⊣⊢@{iProp Σ} ⌜ a1 = a2 ⌝ ∧ (∀ v p', m1 v p' ≡ m2 v p').
+Proof.
+  rewrite /proto_message gmap_equivI /=.
+  iSplit.
+  { destruct (decide (a1=a2)) as [->|Hne]; last first.
+    { iIntros "H". iSpecialize ("H" $! a1).
+      rewrite lookup_insert. rewrite lookup_insert_ne; [|done].
+      by rewrite option_equivI. }
+    iIntros "H". iSpecialize ("H" $! a2).
+    rewrite !lookup_insert option_equivI.
+    iSplit; [done|].
+    iIntros (v p). rewrite discrete_fun_equivI.
+    iSpecialize ("H" $! v).
+    rewrite ofe_morO_equivI=> /=.
+    iSpecialize ("H" $! (laterO_map proto_unfold p)).
+    assert (p ≡ later_map proto_fold (later_map proto_unfold p)) as <-; last by done.
+    rewrite -later_map_compose. rewrite -(later_map_id p).
+    apply later_map_ext=> p' /=. by rewrite proto_fold_unfold. }
+  iIntros "[%Heq H2]" (i). rewrite Heq.
+  destruct (decide (a2 = i)) as [->|Hneq]; [|by rewrite !lookup_insert_ne].
+  rewrite !lookup_insert option_equivI discrete_fun_equivI.
+  iIntros (v). rewrite ofe_morO_equivI. by iIntros (p).
+Qed.
+Lemma proto_message_end_equivI  {Σ} {V} `{!Cofe PROPn, !Cofe PROP} a m :
+  proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a m ≡ proto_end ⊢@{iProp Σ} False.
+Proof.
+  rewrite /proto_message /proto_end. rewrite gmap_equivI.
+  iIntros "H". iSpecialize ("H" $! a). rewrite lookup_insert. rewrite lookup_empty.
+  by rewrite option_equivI.
+Qed.
+Lemma proto_end_message_equivI {Σ} {V} `{!Cofe PROPn, !Cofe PROP} a m :
+  proto_end ≡ proto_message (V:=V) (PROPn:=PROPn) (PROP:=PROP) a m ⊢@{iProp Σ} False.
 Proof. by rewrite internal_eq_sym proto_message_end_equivI. Qed.
 
 (** Functor *)