proposition: Lemma map_eq_name_eq_eq : forall l l', map tot_map_name l = map tot_map_name l' -> l = l'.
proof: Proof. Proof using name_map_bijective. elim. case => //=. move => n l IH. case => //=. move => n' l' H_eq. inversion H_eq. find_apply_lem_hyp tot_map_name_injective. find_eapply_lem_hyp IH. by repeat find_rewrite. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)