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