proposition: Lemma not_in_map_not_in_failed : forall failed n, ~ In n (map tot_map_name failed) -> ~ In (tot_map_name_inv n) failed.
proof: Proof. Proof using name_map_bijective. elim => //=. move => n ns IH n' H_in H_in'. case: H_in' => H_in'. case: H_in. left. by rewrite H_in' tot_map_name_inverse_inv. contradict H_in'. apply: IH. move => H_in'. case: H_in. by right. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)