proposition: Lemma step_star_app_one: forall s h l s'', step_star s (h ++ [l]) s'' <-> exists s', step_star s h s' /\ step s' l s''.
proof: Proof. intros. assert (L := step_star_app). specialize (L s h [l] s''). split; intros. destruct L as [L _]. depremise L. assumption. destruct L as [s' [L1 L2]]. assert (L := step_star_one). specialize (L s' l s''). destruct L as [L _]. depremise L. assumption. exists s'. split; assumption. destruct L as [_ L]. depremise L. destruct H as [s' [H1 H2]]. exists s'. split. assumption. assert (L := step_star_one). specialize (L s' l s''). destruct L as [_ L]. depremise L. assumption. assumption. assumption. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)