proposition: Lemma lsteps_nil_cons s S: star lstep nil (s :: S) -> False.
proof: Proof. intros H. inv H. eapply lstep_nil_cons; eauto. Qed.
imports: List Morphisms FinFun Undecidability.HOU(std.tactics std.ars.basic std.ars.confluence)