proposition: Lemma hd_error_filterMap_pt_map_msg : forall l m' m0, pt_map_msg m0 = Some m' -> hd_error l = Some m0 -> hd_error (filterMap pt_map_msg l) = Some m'.
proof: Proof. Proof using. case => //=. move => m l m' m0 H_eq H_eq'. find_injection. by break_match. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)