proposition: Lemma lsteps_cons_nil s S: star lstep (s :: S) nil -> False.
proof: Proof. intros. remember (s :: S) as S'. remember nil as T. revert S s HeqS' HeqT. induction H. - intros; subst; discriminate. - intros; subst. inv H; eapply IHstar; eauto. Qed.
imports: List Morphisms FinFun Undecidability.HOU(std.tactics std.ars.basic std.ars.confluence)