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