proposition: Lemma pt_in_tot_map_name : forall m m' l n, pt_map_msg m = Some m' -> (forall nm, In nm l -> snd nm = m) -> In (n, m') (filterMap pt_map_name_msg l) -> In (tot_map_name_inv n, m) l.
proof: Proof. Proof using name_map_bijective. move => m m'. elim => //=. case => /= n m0 l IH n' H_eq 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'. rewrite tot_map_name_inv_inverse. have H_nm := H_in (n, m0). rewrite -H_nm /=; first by left. by left. right. apply: IH => //. move => nm H_inn. apply: H_in. by right. move => H_in'. right. apply: IH => //. move => nm H_inn. apply: H_in. by right. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)