proposition: Lemma pt_map_in_in : forall m m0 n l, (forall nm, In nm l -> snd nm = m) -> ~ In (n, m) l -> ~ In (tot_map_name n, m0) (filterMap pt_map_name_msg l).
proof: Proof. Proof using name_map_bijective. move => m m0 n. elim => //=. case => /= n' m' l IH H_fail H_in. rewrite /pt_map_name_msg /=. case H_m: (pt_map_msg _) => [m1|]. move => H_in'. case: H_in' => H_in'. inversion H_in'. have H_nm := H_fail (n', m'). rewrite /= in H_nm. case: H_in. left. apply tot_map_name_injective in H0. rewrite H0. rewrite H_nm //. by left. contradict H_in'. apply: IH. move => nm H_in_nm. apply: H_fail. by right. move => H_in_nm. case: H_in. by right. apply: IH. move => nm H_in'. apply: H_fail => //. by right. move => H_in'. case: H_in. by right. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)