apply confl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ joins R y z
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y z : A
red_x_y : R x y
red_x_z : R x z
⊢ wedge R y z