exists y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y : A
red_x_y : R x y
⊢ joins R x y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y : A
red_x_y : R x y
⊢ refl_trans_clos R x y ∧ refl_trans_clos R y y