proposition: Lemma nodup_to_map_name : forall ns, NoDup ns -> NoDup (map tot_map_name ns).
proof: Proof. Proof using name_map_bijective. elim => /=; first by move => H_nd; exact: NoDup_nil. move => n ns IH H_nd. inversion H_nd. find_apply_lem_hyp IH. by apply NoDup_cons; first exact: not_in_failed_not_in. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)