proposition: Lemma diamond_to_semi_confluent R : diamond R -> semi_confluent R.
proof: Proof. 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 _ _ _ B D) as [v [E F]]. destruct (IH _ F) as [u [G H]]. exists u. eauto using star. Qed.
imports: Undecidability.Shared.Libs.PSL.Base Lia Arith Arith