proposition: Lemma rev_step_star_inv : forall s ls s0 (P : StepStarArgs.State -> list StepStarArgs.Label -> StepStarArgs.State -> Prop), P s nil s -> (forall l s1 ls', StepStarArgs.step s l s1 -> step_star s1 ls' s0 -> P s (l::ls')%list s0) -> step_star s ls s0 -> P s ls s0.
proof: Proof. intros s ls s0 P Hnil Hstep Hss. revert P Hnil Hstep. induction Hss using rev_step_star_ind; intros; auto. eauto. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)