proposition: Lemma count_occ_filterMap_pt_map_msg_eq : forall l m' m0, pt_map_msg m0 = Some m' -> count_occ msg_eq_dec (filterMap pt_map_msg l) m' = count_occ msg_eq_dec l m0.
proof: Proof. Proof using pt_map_msg_injective. elim => //=. move => m l IH m' m0 H_eq. break_if. repeat find_rewrite. rewrite /=. break_if => //. have IH' := IH _ _ H_eq. by rewrite IH'. have IH' := IH _ _ H_eq. rewrite -IH'. break_match => //. rewrite /=. break_if => //. case: n. find_rewrite. move: Heqo H_eq. exact: pt_map_msg_injective. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)