proposition: Lemma not_in_failed_in_exclude : forall ns n failed, ~ In (tot_map_name_inv n) failed -> In (tot_map_name_inv n) ns -> In (tot_map_name_inv n) (remove_all name_eq_dec failed ns).
proof: Proof. Proof using. elim => //=. move => n ns IH n' failed H_in H_in'. have H_cn := remove_all_cons name_eq_dec failed n ns. break_or_hyp; break_and; find_rewrite; break_or_hyp => //=. - exact: IH. - by left. - right; exact: IH. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)