intros x y red_x_y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
⊢ ∀ (x y : A), refl_trans_sym_clos R x y → joins R x y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y : A
red_x_y : refl_trans_sym_clos R x y
⊢ joins R x y