proposition: Lemma fast_check_all_schedules_correct': forall nids N s check check', fast_check_all_schedules nids N s check = true -> (forall l s, check s = true -> check' l s = true) -> check_all_schedules' nids N s check' = true.
proof: Proof. Proof using max_nid_eq. induction N; intros. * reflexivity. * unfold check_all_schedules'; fold check_all_schedules'. unfold fast_check_all_schedules in H; fold fast_check_all_schedules in H. rewrite List.forallb_forall in *. setoid_rewrite Bool.andb_true_iff. setoid_rewrite List.forallb_forall. setoid_rewrite Bool.andb_true_iff in H. setoid_rewrite List.forallb_forall in H. intros n1 Hin1. specialize (H n1 Hin1). mcase_eq. destruct p. apply fast_step_correct in H1. rewrite H1 in H. rewrite Bool.andb_true_iff in *. destruct H as [[??]?]. split_all; auto. eapply IHN; eauto. intros n2 Hin2. mcase_eq; auto. destruct p. apply fast_step_correct in H4. specialize (H3 n2 Hin2). rewrite H4 in H3. rewrite Bool.andb_true_iff in *. destruct H3. split; eauto. split; auto. intros n2 Hin2. mcase_eq; auto. destruct p. apply fast_step_correct in H2. destruct H as [_ H]. specialize (H n2 Hin2). rewrite H2 in H. rewrite Bool.andb_true_iff in *. destruct H. split; eauto. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)