proposition: Lemma confluent_CR R : church_rosser R <-> confluent R.
proof: Proof. split; intros A. - intros x y z B C. apply A. eauto using (@ecl_trans R), star_ecl, (@ecl_sym R). - intros x y B. apply semi_confluent_confluent in A. induction B as [x|x x' y C B IH|x x' y C B IH]. + exists x. eauto using star. + destruct IH as [z [D E]]. exists z. eauto using star. + destruct IH as [u [D E]]. destruct (A _ _ _ C D) as [z [F G]]. exists z. eauto using (@star_trans R). Qed.
imports: Undecidability.Shared.Libs.PSL.Base Lia Arith Arith