proposition: Lemma msg_in_map : forall m l n m', (forall nm, In nm l -> snd nm = m) -> In (tot_map_name n, tot_map_msg m') (map (fun nm : name * msg => (tot_map_name (fst nm), tot_map_msg (snd nm))) l) -> tot_map_msg m' = tot_map_msg m.
proof: Proof. Proof using. move => m. elim => //=. case => /= n m' l IH n' m0 H_in H_in_map. have H_in_f := H_in (n, m'). rewrite /= in H_in_f. case: H_in_map => H_in_map. inversion H_in_map. rewrite H_in_f //. by left. move: H_in_map. apply: IH. move => nm H_in'. apply: H_in. by right. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)