exists y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z a✝ y : A
red✝ : R a✝ y
⊢ joins R y a✝
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
sc : diamond R
x z a✝ y : A
red✝ : R a✝ y
⊢ refl_trans_clos R y y ∧ refl_trans_clos R a✝ y