proposition: Lemma in_pt_map_map_pair : forall m m' l n, pt_map_msg m = Some m' -> (forall nm, In nm l -> snd nm = m) -> In (tot_map_name_inv n, m) l -> In (n, m') (filterMap pt_map_name_msg 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 m0) => [m1|]. move => H_in'. case: H_in' => H_in'. inversion H_in'. rewrite H1 in H_m. rewrite H_m in H_eq. inversion H_eq. left. by rewrite tot_map_name_inverse_inv. right. apply: IH => //. move => nm H_inn. apply: H_in. by right. move => H_in'. case: H_in' => H_in'. inversion H_in'. rewrite H1 in H_m. by rewrite H_m in H_eq. 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)