proposition: Lemma step_star_fun_cons_inv: forall sched s l ls s'', step_star_fun nil sched s = Some (l :: ls, s'')%list -> exists task s' sched', sched = (task::sched')%list /\ step_fun task s = Some (l, s') /\ step_star_fun nil sched' s' = Some (ls, s'').
proof: Proof. Proof using. intros. clear max_nid_eq. revert s l ls s'' H. destruct sched as [ | task sched]; simpl; intros. * inversion H; clear H; subst. * mcase_eq as Hs in H; try discriminate. destruct p. apply prefix_inv_step_star_fun in H as [ls3[Heq Hss]]. simpl in Heq. inversion Heq; clear Heq; subst l0 ls3. exists task; exists s0; exists sched; simpl; split_all; auto. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)