proposition: Lemma in_tot_map_msg : forall m l n, (forall nm, In nm l -> snd nm = m) -> In (tot_map_name_inv n, m) l -> In (n, tot_map_msg m) (map (fun nm : name * msg => (tot_map_name (fst nm), tot_map_msg (snd nm))) l).
proof: Proof. Proof using name_map_bijective. move => m. elim => //=. case => n m' /= l IH n' H_in H_in'. case: H_in' => H_in'. inversion H_in'. left. by rewrite tot_map_name_inverse_inv. right. apply: IH => //. move => nm H_inn. apply: H_in. by right. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)