fact: Fixpoint step_star_fun tracePrefix (sched : list ScheduleTask) s : option ((list Label) * State) := match sched with | task :: sched' => match step_fun task s with | Some (l, s') => step_star_fun (tracePrefix++[l]) sched' s' | None => None end | nil => Some (tracePrefix, s) end%list.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)