proposition: Lemma step_star_app: forall s h1 h2 s'', step_star s (h1 ++ h2) s'' <-> exists s', step_star s h1 s' /\ step_star s' h2 s''.
proof: Proof. intros. split. intros. generalize dependent s. generalize dependent h2. induction h1. intros. rewrite app_nil_l in H. exists s. split. apply refl. assumption. intros. rewrite <- app_comm_cons in H. apply step_star_end in H. destruct H as [s' [H1 H2]]. specialize (IHh1 h2 s'). depremise IHh1. assumption. destruct IHh1 as [sm [IHh1 IHh2]]. exists sm. split. apply step_star_end. exists s'. split; assumption. assumption. intros. generalize dependent s. generalize dependent h2. induction h1. intros. destruct H as [s' [H1 H2]]. rewrite app_nil_l. inversion H1. subst. assumption. subst. destruct ls. rewrite app_nil_l in H. inversion H. inversion H. intros. destruct H as [s' [H1 H2]]. apply step_star_end in H1. destruct H1 as [sm [H11 H12]]. specialize (IHh1 h2 sm). depremise IHh1. exists s'. split; assumption. rewrite <- app_comm_cons. eapply step_star_end. exists sm. split; assumption. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)