fact: Definition add_ghost_msg (me : name) (st : data) (ps : list (name * msg)) : list (name * (ghost_msg * msg)) := map (fun m => (fst m, (write_ghost_msg me st, snd m))) ps.
imports: Coq(List) StructTact(StructTactics Util) Verdi(Net TotalMapSimulations) Coq(FunctionalExtensionality) Verdi(Ssrexport)