proposition: Lemma normal_in_lstep A: (forall x, In x A -> Normal R x) -> Normal lstep A.
proof: Proof. induction A; cbn; intuition idtac. - intros ? H1. inv H1. - intros ? H1. inv H1. eapply H; eauto. eapply IHA; eauto. Qed.
imports: List Morphisms FinFun Undecidability.HOU(std.tactics std.ars.basic std.ars.confluence)