fact: Definition valid_schedule nids (sched: list ScheduleTask) := List.Forall (fun task => match task with | SchedProc n1 => List.In n1 nids | SchedUpdate n1 n2 => List.In n1 nids /\ List.In n2 nids end) sched.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)