proposition: Lemma step_star_fun_app: forall sched1 sched2 ls1 s, step_star_fun ls1 (sched1 ++ sched2)%list s = match step_star_fun ls1 sched1 s with | Some (ls2, s') => step_star_fun ls2 sched2 s' | None => None end.
proof: Proof. Proof using. clear max_nid_eq. induction sched1; simpl; intros; auto. repeat mcase_eq; subst; auto. rewrite IHsched1, H1; reflexivity. rewrite IHsched1, H1; reflexivity. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)