proposition: Lemma step_star_fun_sound: forall sched s ls1 ls2 s', step_star_fun ls1 sched s = Some (ls1++ls2,s')%list -> step_star s ls2 s'.
proof: Proof. Proof using max_nid_eq. intros sched s ls1 ls2 s' Hss. revert s ls1 ls2 s' Hss. induction sched; simpl; intros. inversion Hss; clear Hss; subst s'; try subst. * rewrite <- app_nil_r in H0 at 1. apply List.app_inv_head in H0; subst ls2. constructor. * case_eq (step_fun a s). intros [??] Hs; rewrite Hs in *. edestruct prefix_inv_step_star_fun as [ls3[Heq _]]; eauto. rewrite <-List.app_assoc in Heq. apply List.app_inv_head in Heq; subst ls2. rewrite List.app_assoc in Hss. apply IHsched in Hss. apply step_fun_sound in Hs. eapply step_star_end; eauto. intro Hs; rewrite Hs in *; discriminate. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)