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