proposition: Lemma in_in_adj_map_pair : forall (m : msg) ns failed n h, In n ns -> ~ In n (map tot_map_name failed) -> adjacent_to h n -> In (n, m) (map2snd m (filter_rel adjacent_to_dec h (remove_all name_eq_dec (map tot_map_name failed) ns))).
proof: Proof. Proof using. move => m. elim => //=. move => n ns IH failed n' h. set mfailed := map _ failed. move => H_in H_in' H_adj. have H_cn := remove_all_cons name_eq_dec mfailed n ns. break_or_hyp; break_and; find_rewrite. break_or_hyp => //. exact: IH. case: H_in => H_in. rewrite H_in. rewrite /=. case (adjacent_to_dec _ _) => H_dec' //. rewrite /=. by left. rewrite /=. case (adjacent_to_dec _ _) => H_dec'. rewrite /=. right. exact: IH. exact: IH. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)