proposition: Lemma in_map_pair_adjacent_to : forall (m : @msg _ multi_fst) ns failed h n, In (tot_map_name_inv n, m) (map2snd m (filter_rel adjacent_to_dec h (remove_all name_eq_dec failed ns))) -> In (tot_map_name_inv n) (filter_rel adjacent_to_dec h (remove_all name_eq_dec failed ns)).
proof: Proof. Proof using. move => m. elim => //= [|n l IH] failed h n'; 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. inversion H_in. by left. right. exact: IH. exact: IH. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)