proposition: Lemma in_exclude_not_in_failed_map : forall ns n failed, In n (remove_all name_eq_dec (map tot_map_name failed) ns) -> ~ In n (map tot_map_name failed) /\ In n ns.
proof: Proof. Proof using. elim => [|n ns IH] n' failed; first by rewrite remove_all_nil. set mfailed := map _ failed. have H_cn := remove_all_cons name_eq_dec mfailed n ns. break_or_hyp; break_and; find_rewrite. move => H_in. apply IH in H_in. move: H_in => [H_nin H_in]. split => //. by right. rewrite /=. move => H_in. case: H_in => H_in. rewrite H_in. subst. split => //. by left. apply IH in H_in. move: H_in => [H_nin H_in]. split => //. by right. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)