proposition: Lemma not_in_failed_not_in : forall n failed, ~ In n failed -> ~ In (tot_map_name n) (map tot_map_name failed).
proof: Proof. Proof using name_map_bijective. move => n. elim => //=. move => n' failed IH H_in H_in'. case: H_in' => H_in'. case: H_in. left. rewrite -(tot_map_name_inv_inverse n'). rewrite H_in'. exact: tot_map_name_inv_inverse. 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)