proposition: Lemma prefix_inv_step_star_fun: forall sched ls1 ls2 s s', step_star_fun ls1 sched s = Some (ls2, s') -> (exists ls3, ls2 = ls1 ++ ls3 /\ step_star_fun nil sched s = Some (ls3, s'))%list.
proof: Proof. Proof using. induction sched; simpl; intros. - inversion H; clear H; subst. exists nil; rewrite List.app_nil_r; split; reflexivity. - destruct (step_fun a s) as [[?]|]; try discriminate. edestruct IHsched as [ls3[??]]; eauto; subst ls2. exists (l::ls3)%list; split. * rewrite <-List.app_assoc. reflexivity. * eapply prefix_step_star_fun with (ls3:=[l]) (ls1:=nil). assumption. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)