proposition: Lemma tot_map_name_injective : forall n n', tot_map_name n = tot_map_name n' -> n = n'.
proof: Proof. Proof using MB. move => n n'. case (name_eq_dec n n') => H_dec //. move => H_eq. case: H_dec. by rewrite -(tot_map_name_inv_inverse n) H_eq tot_map_name_inv_inverse. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)