proposition: Lemma adjacent_in_in_msg : forall (m : @msg base_fst multi_fst) ns n h, adjacent_to h (tot_map_name_inv n) -> In (tot_map_name_inv n) ns -> In (tot_map_name_inv n, m) (map2snd m (filter_rel adjacent_to_dec h ns)).
proof: Proof. Proof using. move => m. elim => //=. move => n ns IH n' h H_adj H_in. case: (adjacent_to_dec _ _) => H_dec; case: H_in => H_in. - rewrite /=. left. by rewrite H_in. - rewrite /=. right. exact: IH. - by rewrite H_in in H_dec. - exact: IH. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)