proposition: Lemma lstep_normal_cons a A: Normal R a -> Normal lstep A -> Normal lstep (a :: A).
proof: Proof. intros ? ? ? ?. inv H1; firstorder. Qed.
imports: List Morphisms FinFun Undecidability.HOU(std.tactics std.ars.basic std.ars.confluence)