proposition: Lemma nodup_pt_map : forall m nms, (forall nm, In nm nms -> snd nm = m) -> NoDup nms -> NoDup (filterMap pt_map_name_msg nms).
proof: Proof. Proof using name_map_bijective. move => m. elim => /=. move => H_m H_nd. exact: NoDup_nil. case => n m0 l IH H_m H_nd. inversion H_nd. rewrite /=. have H_m0 := H_m (n, m0) (or_introl (eq_refl _)). rewrite /= in H_m0. rewrite H_m0. rewrite H_m0 {m0 H_m0} in H_m H_nd H1 H. rewrite /pt_map_name_msg /=. case H_m': (pt_map_msg _) => [m'|]. apply NoDup_cons. apply: (@pt_map_in_in m) => //. move => nm H_in. by apply: H_m; right. apply: IH => //. move => nm H_in. by apply: H_m; right. apply: IH => //. move => nm H_in. by apply: H_m; right. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)