fact: Definition tot_mapped_lb_input_handlers_label me inp st := let '(lb, out, st', ps) := lb_input_handlers me inp st in tot_map_label lb.
imports: Verdi(Verdi LabeledNet TotalMapSimulations) InfSeqExt(infseq map exteq) Coq(FunctionalExtensionality) Verdi(Ssrexport)