proposition: Lemma tot_map_name_in : forall ns n, In (tot_map_name n) (map tot_map_name ns) -> In n ns.
proof: Proof. Proof using name_map_bijective. elim => //=. move => n' ns IH n H_in. case: H_in => H_in. left. exact: tot_map_name_injective. right. exact: IH. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)