proposition: Lemma step_star_end: forall s l h s'', step_star s (l :: h) s'' <-> exists s', step s l s' /\ step_star s' h s''.
proof: Proof. intros. split; intros. generalize dependent s''. induction h using rev_ind. intros. exists s''. split. inversion H. subst. rewrite <- app_nil_l in H0. apply app_inj_tail in H0. destruct H0; subst. inversion H1. subst. assumption. subst. apply app_eq_nil in H0. destruct H0; subst. inversion H4. constructor. intros. rewrite app_comm_cons in H. inversion H. rewrite app_comm_cons in H0. apply app_inj_tail in H0. destruct H0. subst. apply IHh in H1. destruct H1 as [s' [N1 N2]]. exists s'. split. assumption. econstructor; eassumption. generalize dependent s''. induction h using rev_ind. intros. destruct H as [s' [H1 H2]]. inversion H2. subst. clear H2. assert (A := steps s nil s l s''). depremise A. constructor. depremise A. assumption. rewrite app_nil_l in A. assumption. subst. apply app_eq_nil in H. destruct H. inversion H3. intros. destruct H as [s' [H1 H2]]. remember (h ++ [x]) as hh eqn: Hh. destruct H2. symmetry in Hh. apply app_eq_nil in Hh. destruct Hh. subst. inversion H0. apply app_inj_tail in Hh. destruct Hh. subst. specialize (IHh s2). depremise IHh. exists s1. split. assumption. assumption. rewrite app_comm_cons. econstructor; eassumption. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)