fact: Definition refined_input_handlers me inp st := let '(out, st', ps) := input_handlers me inp (snd st) in (out, (ghost_input_handlers me inp st, st'), ps).
imports: Coq(List) StructTact(StructTactics Util) Verdi(Net TotalMapSimulations) Coq(FunctionalExtensionality) Verdi(Ssrexport)