fact: Definition refined_init_handlers (n : name) : ghost_data * data := (ghost_init, init_handlers n).
imports: Coq(List) StructTact(StructTactics Util) Verdi(Net TotalMapSimulations) Coq(FunctionalExtensionality) Verdi(Ssrexport)