proposition: Lemma lstep_normal_cons_l a A: Normal lstep (a :: A) -> Normal R a.
proof: Proof. intros ? ? ?. eapply H; econstructor; eauto. Qed.
imports: List Morphisms FinFun Undecidability.HOU(std.tactics std.ars.basic std.ars.confluence)