fact: Fixpoint fast_step_star_fun (sched : list ScheduleTask) s : option State := match sched with | task :: sched' => match fast_step_fun task s with | Some s' => fast_step_star_fun sched' s' | None => None end | nil => Some s end%list.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)