proposition: Lemma nodup_tot_map : forall m nms, (forall nm, In nm nms -> snd nm = m) -> NoDup nms -> NoDup (map (fun nm : name * msg => (tot_map_name (fst nm), tot_map_msg (snd nm))) nms).
proof: Proof. Proof using name_map_bijective. move => m'. elim => /=. move => H_fail H_nd. exact: NoDup_nil. case => n m l IH H_fail H_nd. inversion H_nd. rewrite /=. apply NoDup_cons. have H_f := H_fail (n, m). rewrite /= in H_f. move => H_in. have H_inf := @msg_in_map m' _ _ _ _ H_in. rewrite H_inf in H_in. contradict H_in. apply tot_map_in_in. move => nm H_in_nm. apply: H_fail. by right. rewrite H_f // in H1. by left. move => nm H_in_f. apply: H_fail. by right. apply: IH => //. move => nm H_in_nm. apply: H_fail. by right. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)