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