proposition: Lemma step_star_fun_complete: forall s ls s', step_star s ls s' -> exists sched, step_star_fun nil sched s = Some (ls,s').
proof: Proof. Proof using max_nid_eq. intros s ls s' Hss. induction Hss using rev_step_star_ind. exists nil; reflexivity. destruct IHHss as [sched ?]. edestruct step_fun_complete as [task ?]; eauto. exists (task::sched)%list. simpl. rewrite H1. rewrite <-List.app_nil_r with (l:=[l]). change (l::ls)%list with ([l]++ls)%list. apply prefix_step_star_fun; auto. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)