proposition: Lemma rev_step_star_ind : forall (P : StepStarArgs.State -> list StepStarArgs.Label -> StepStarArgs.State -> Prop), (forall s, P s nil s) -> (forall s1 l s2 ls s3, StepStarArgs.step s1 l s2 -> step_star s2 ls s3 -> P s2 ls s3 -> P s1 (l::ls)%list s3) -> forall s l s0, step_star s l s0 -> P s l s0.
proof: Proof. intros P Hnil Hstep. intros s l1 s1 Hss1. assert (Hss2: step_star s1 nil s1) by auto. remember s1 as s0 in Hss2 at 2. rewrite <-Heqs0. remember nil as l2 in Hss2. replace l1 with (l1++l2)%list by (subst; rewrite List.app_nil_r; auto). assert (HPl2: P s1 l2 s0) by (subst; auto). clear Heqs0 Heql2. revert s0 l2 HPl2 Hss2. induction Hss1; intros; auto. rewrite <-List.app_assoc. apply IHHss1. eapply Hstep; eauto. simpl. apply step_star_end. eauto. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)