proposition: Lemma prefix_step_star_fun: forall sched ls1 ls2 ls3 s s', step_star_fun ls1 sched s = Some (ls2, s') -> step_star_fun (ls3++ls1)%list sched s = Some (ls3++ls2, s')%list.
proof: Proof. Proof using. induction sched; simpl; intros. congruence. destruct (step_fun a s ) as [ [??] | ]; try discriminate. rewrite <-List.app_assoc. eauto. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)