proposition: Lemma valid_schedule_app: forall nids sched1 sched2, valid_schedule nids (sched1++sched2) <-> valid_schedule nids sched1 /\ valid_schedule nids sched2.
proof: Proof. Proof using. unfold valid_schedule; intros. rewrite !List.Forall_forall in *. setoid_rewrite List.in_app_iff. split. * intros H. split; intros task Hin; specialize (H task); tauto. * intros [H1 H2] x. specialize (H1 x); specialize (H2 x). intros [?|?]; tauto. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)