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