proposition: Lemma in_tot_map_name : forall m l n, (forall nm, In nm l -> snd nm = m) -> In (n, tot_map_msg m) (map (fun nm : name * msg => (tot_map_name (fst nm), tot_map_msg (snd nm))) l) -> In (tot_map_name_inv n, m) 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'. rewrite tot_map_name_inv_inverse. have H_nm := H_in (n, m'). rewrite -H_nm /=; first by left. by left. 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)