proposition: Lemma step_star_one: forall s l s', step_star s [l] s' <-> step s l s'.
proof: Proof. intros; split; intros. inversion H. destruct ls. subst. rewrite app_nil_l in H0. inversion H0. subst. inversion H1. subst. assumption. destruct ls. rewrite app_nil_l in H2. inversion H2. inversion H2. inversion H0. destruct ls. rewrite app_nil_l in H7. inversion H7. inversion H7. assert (A : [l] = nil ++ [l]). apply app_nil_l. rewrite A in *; clear A. eapply steps. constructor. assumption. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)