proposition: Lemma tot_map_in_snd : forall h m ns nm, In nm (map (fun nm0 : name * msg => (tot_map_name (fst nm0), tot_map_msg (snd nm0))) (map2snd m (filter_rel adjacent_to_dec h ns))) -> snd nm = tot_map_msg m.
proof: Proof. Proof using. move => h m. elim => //=. move => n ns IH. case: (adjacent_to_dec _ _) => H_dec /=. case => n' m' H_in. case: H_in => H_in. by inversion H_in. exact: IH. exact: IH. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)