From mathcomp.ssreflect
Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.
From mathcomp
Require Import path.
Require Import Eqdep.
Require Import Relation_Operators.
From fcsl
Require Import pred prelude ordtype finmap pcm unionmap heap.
From DiSeL
Require Import Freshness State EqTypeX DepMaps.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section NewSoupPredicates.

(*****************************************************)
(*        More elaborated message predicates         *)
(*****************************************************)


(* Goal: @ex (Ordered.sort mid) (@unique (Ordered.sort mid) (fun i0 : Ordered.sort mid => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))))) *)
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
Definition msg_in_soup' from to t (cond : seq nat -> bool) (d : soup) :=
  (exists! i, exists c,
        find i d = Some (Msg (TMsg t c) from to true)) /\
(* Goal: @ex (Ordered.sort mid) (@unique (Ordered.sort mid) (fun i0 : Ordered.sort mid => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))))) *)
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
  forall i c, find i d = Some (Msg (TMsg t c) from to true) -> cond c.

Definition msg_spec' from to tg cnt :=
  msg_in_soup' from to tg (fun y => (y == cnt)).

Definition no_msg_from_to' from to
(* Goal: @ex (Ordered.sort mid) (@unique (Ordered.sort mid) (fun i0 : Ordered.sort mid => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))))) *)
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
           (criterion : nat -> seq nat -> bool) (d : soup) :=
  forall i t c,
(* Goal: @ex (Ordered.sort mid) (@unique (Ordered.sort mid) (fun i0 : Ordered.sort mid => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))))) *)
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
    find i d = Some (Msg (TMsg t c) from to true) -> ~~criterion t c.

Lemma no_msg_from_to_consume' from to cond s i:
(* Goal: @ex (Ordered.sort mid) (@unique (Ordered.sort mid) (fun i0 : Ordered.sort mid => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))))) *)
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
  valid s ->
(* Goal: @ex (Ordered.sort mid) (@unique (Ordered.sort mid) (fun i0 : Ordered.sort mid => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))))) *)
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
  no_msg_from_to' from to cond s ->
  no_msg_from_to' from to cond (consume_msg s i).
Proof.
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
move=>V H m t c .
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) k (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c1) from to true)), is_true (cond c1) *)
rewrite /consume_msg; case: (find i s); last by move=>F; apply: (H m t c F).
(* Goal: forall (a : msg TaggedMessage) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) m (@UMC.upd mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i (@mark_msg TaggedMessage a) s)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (negb (cond t c)) *)
move=>ms; case B: (m == i).
(* Goal: @ex (Ordered.sort mid) (@unique (Ordered.sort mid) (fun i0 : Ordered.sort mid => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))))) *)
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
- by move/eqP: B=>B; subst m; rewrite findU eqxx/= V.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) k (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c1) from to true)), is_true (cond c1) *)
by rewrite findU B/==>/(H m t c).
Qed.

Lemma no_msg_spec_consume s from to tg cnt cond i :
(* Goal: @ex (Ordered.sort mid) (@unique (Ordered.sort mid) (fun i0 : Ordered.sort mid => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))))) *)
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
  valid s ->
  find i s = Some {| content := TMsg tg cnt;
(* Goal: @ex (Ordered.sort mid) (@unique (Ordered.sort mid) (fun i0 : Ordered.sort mid => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))))) *)
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
                     from := from; to := to; active := true |} ->
(* Goal: @ex (Ordered.sort mid) (@unique (Ordered.sort mid) (fun i0 : Ordered.sort mid => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))))) *)
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
  msg_in_soup' from to tg cond s ->
  no_msg_from_to' from to (fun x y => (x == tg)) (consume_msg s i).
Proof.
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
move=>V F[][j][[c]]F' H1 H2.
(* Goal: no_msg_from_to' from to (fun (x : nat) (_ : list nat) => @eq_op nat_eqType x tg) (consume_msg s i) *)
move=>m t' c'; rewrite /consume_msg; move: (find_some F).
(* Goal: @ex (Ordered.sort mid) (@unique (Ordered.sort mid) (fun i0 : Ordered.sort mid => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))))) *)
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
case: dom_find=>// msg->_ _; case B: (m == i).
(* Goal: @ex (Ordered.sort mid) (@unique (Ordered.sort mid) (fun i0 : Ordered.sort mid => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))))) *)
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
- by move/eqP: B=>B; subst m; rewrite findU eqxx/= V.
(* Goal: msg_in_soup' from to t cond (consume_msg d i) *)
have X: j = i by apply: (H1 i); exists cnt.
(* Goal: forall _ : @eq (option (State.msg TaggedMessage)) (@UMC.find mid (State.msg TaggedMessage) (union_mapUMC mid (State.msg TaggedMessage)) m (@UMC.upd mid (State.msg TaggedMessage) (union_mapUMC mid (State.msg TaggedMessage)) i (@mark_msg TaggedMessage msg) s)) (@Some (State.msg TaggedMessage) (@Msg TaggedMessage (TMsg t' c') from to true)), is_true (negb (@eq_op nat_eqType t' tg)) *)
subst j; rewrite findU B/==>H.
(* Goal: @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
case X: (t' == tg)=>//=.
(* Goal: is_true false *)
move/eqP: X=>X; subst t'. 
(* Goal: is_true false *)
suff X: i = m by subst i; rewrite eqxx in B.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) k (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c1) from to true)), is_true (cond c1) *)
by apply: (H1 m); exists c'.  
Qed.

Lemma msg_spec_consumeE i d from to from' to' t c' t' cond:
(* Goal: @ex (Ordered.sort mid) (@unique (Ordered.sort mid) (fun i0 : Ordered.sort mid => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))))) *)
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
  valid d ->
(* Goal: @ex (Ordered.sort mid) (@unique (Ordered.sort mid) (fun i0 : Ordered.sort mid => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))))) *)
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
  find  i d = Some (Msg (TMsg t' c') from' to' true) ->
(* Goal: @ex (Ordered.sort mid) (@unique (Ordered.sort mid) (fun i0 : Ordered.sort mid => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))))) *)
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
  msg_in_soup' from to t cond d ->
(* Goal: @ex (Ordered.sort mid) (@unique (Ordered.sort mid) (fun i0 : Ordered.sort mid => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))))) *)
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
  [|| (from != from'), (to != to') | (t != t')] ->
  msg_in_soup' from to t cond (consume_msg d i).
Proof.
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
move=>V E S N.
(* Goal: @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
case: S=>[][j][[c]F]H1 H2.
(* Goal: msg_in_soup' from to t cond (consume_msg d i) *)
have Nij: i != j.
(* Goal: @ex (Ordered.sort mid) (@unique (Ordered.sort mid) (fun i0 : Ordered.sort mid => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))))) *)
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
- case H: (i == j)=>//.
(* Goal: is_true (negb true) *)
(* Goal: msg_in_soup' from to t cond (consume_msg d i) *)
  move/eqP in H; subst i; move: E; rewrite F=>[][???]; subst.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) k (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c1) from to true)), is_true (cond c1) *)
  move: N=>/orP []/eqP; first by congruence.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) k (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c1) from to true)), is_true (cond c1) *)
  move/eqP/orP; case; first by move=>X Z; subst to'; rewrite eqxx in X. 
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) k (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c1) from to true)), is_true (cond c1) *)
  by rewrite eqxx.
(* Goal: msg_in_soup' from to t cond (consume_msg d i) *)
split.
(* Goal: @ex (Ordered.sort mid) (@unique (Ordered.sort mid) (fun i0 : Ordered.sort mid => @ex (list nat) (fun c : list nat => @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))))) *)
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
- exists j; split; first by exists c; rewrite mark_other// eq_sym; apply/negbTE.
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
  move=> x [c1][E'].
(* Goal: @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
  case H: (x == i).
(* Goal: @eq (Ordered.sort mid) j x *)
(* Goal: @eq (Ordered.sort mid) j x *)
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
  + by move/eqP in H; subst x; rewrite (find_consume _ E) in E'. 
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) k (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c1) from to true)), is_true (cond c1) *)
  by apply: H1; exists c1; rewrite mark_other in E'.
(* Goal: forall (i0 : Ordered.sort mid) (c : list nat) (_ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) i0 (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c) from to true))), is_true (cond c) *)
move=>k c1.
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) k (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c1) from to true)), is_true (cond c1) *)
case H: (k == i); first by move/eqP in H; subst k; rewrite (find_consume _ E).  
(* Goal: forall _ : @eq (option (msg TaggedMessage)) (@UMC.find mid (msg TaggedMessage) (union_mapUMC mid (msg TaggedMessage)) k (consume_msg d i)) (@Some (msg TaggedMessage) (@Msg TaggedMessage (TMsg t c1) from to true)), is_true (cond c1) *)
by rewrite mark_other//; apply: H2.
Qed.


End NewSoupPredicates.
