proposition: Lemma pt_map_in_snd : forall m m' h ns nm, pt_map_msg m' = Some m -> In nm (filterMap pt_map_name_msg (map2snd m' (filter_rel adjacent_to_dec h ns))) -> snd nm = m.
proof: Proof. Proof using. move => m m' h. elim => //=. move => n ns IH. case: (adjacent_to_dec _ _) => H_dec /=; last exact: IH. case => n' m0 H_eq. rewrite /pt_map_name_msg /=. case H_eq': (pt_map_msg m') => [m1|]; last by rewrite H_eq' in H_eq. rewrite H_eq' in H_eq. inversion H_eq. rewrite H0 in H_eq'. move {H_eq H0 m1}. move => H_in. case: H_in => H_in; first by inversion H_in. exact: (IH (n', m0)). Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)