proposition: Lemma pt_msg_in_map : forall m l n m', (forall nm, In nm l -> snd nm = m) -> In (tot_map_name n, m') (filterMap pt_map_name_msg l) -> pt_map_msg m = Some m'.
proof: Proof. Proof using. move => m. elim => //=. case => /= n m' l IH n' m0 H_in. rewrite /pt_map_name_msg /=. case H_m: (pt_map_msg m') => [m1|]. have H_in_f := H_in (n, m'). rewrite /= in H_in_f. move => H_in_map. case: H_in_map => H_in_map. inversion H_in_map. rewrite H_in_f in H_m; last by left. by rewrite -H1. move: H_in_map. apply: (IH _ m0) => //. move => nm H_in'. apply: H_in. by right. apply: (IH _ m0) => //. move => nm H_in'. apply: H_in => //. by right. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)