proposition: Lemma in_all_before_pt_map_msg : forall l m0 m1 m'0 m'1, pt_map_msg m0 = Some m'0 -> pt_map_msg m1 = Some m'1 -> before_all m'0 m'1 (filterMap pt_map_msg l) -> before_all m0 m1 l.
proof: Proof. Proof using. elim => //=. move => m l IH m0 m1 m'0 m'1 H_eq H_eq' H_bef. break_match; simpl in *. case: H_bef => H_bef. left. move => H_in. case: H_bef. move: H_eq H_in. exact: in_msg_filterMap_pt_map_msg. break_and. right. split; last first. move: H0. exact: IH. move => H_eq_m. rewrite H_eq_m in H_eq'. rewrite Heqo in H_eq'. by find_injection. right. split; last first. move: H_bef. exact: IH. by congruence. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)