intros x y z r_x_y r_x_z
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ weakly_confluent RX
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
r_x_y : RX x y
r_x_z : RX x z
⊢ joins RX y z