proposition: Lemma tot_map_in_in : forall n m l, (forall nm, In nm l -> snd nm = m) -> ~ In (n, m) l -> ~ In (tot_map_name 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 => n m. elim => //=. case => /= n' m' l IH H_eq H_in. move => H_in'. case: H_in' => H_in'. inversion H_in'. have H_nm := H_eq (n', m'). rewrite /= in H_nm. case: H_in. left. apply tot_map_name_injective in H0. rewrite H0. rewrite H_nm //. by left. contradict H_in'. apply: IH. move => nm H_in_nm. apply: H_eq. by right. move => H_in_nm. case: H_in. by right. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)