proposition: Lemma confluence_lstep: confluent R -> confluent lstep.
proof: Proof. intros conf ?. induction x; intros. - inv H. inv H0. exists nil; eauto. inv H. inv H1. - destruct y, z; try solve [exfalso; eapply lsteps_cons_nil; eassumption]. eapply lsteps_cons_inv in H; eapply lsteps_cons_inv in H0. intuition idtac; destruct (IHx _ _ H2 H3) as [V]. destruct (conf _ _ _ H1 H) as [v]. exists (v :: V). now rewrite H5, H0. now rewrite H6, H4. Qed.
imports: List Morphisms FinFun Undecidability.HOU(std.tactics std.ars.basic std.ars.confluence)