proposition: Lemma in_msg_filterMap_pt_map_msg : forall l m' m0, pt_map_msg m0 = Some m' -> In m0 l -> In m' (filterMap pt_map_msg l).
proof: Proof. Proof using. elim => //. move => m0 l IH. move => m1 m2 H_eq H_in. case: H_in => H_in. rewrite H_in /= H_eq. by left. have IH' := IH _ _ H_eq H_in. rewrite /=. by break_match; first by right. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)