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