proposition: Lemma valid_schedule_cons: forall nids task sched, valid_schedule nids (task::sched) <-> match task with | SchedProc n1 => List.In n1 nids | SchedUpdate n1 n2 => List.In n1 nids /\ List.In n2 nids end /\ valid_schedule nids sched.
proof: Proof. Proof using. unfold valid_schedule; intros. split; intros. inversion H; split; auto. apply List.Forall_cons; tauto. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)