proposition: Lemma fast_step_star_correct: forall ls sched s ls' s', step_star_fun ls sched s = Some (ls', s') -> fast_step_star_fun sched s = Some s'.
proof: Proof. Proof using max_nid_eq. intros. revert ls s ls' s' H. induction sched; simpl; intros. * congruence. * mcase_eq as Hs in H; try congruence. destruct p. apply fast_step_correct in Hs; rewrite Hs. eauto. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)