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