cases h
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
h : refl_trans_clos R x z ∧ refl_trans_clos R y z
⊢ joins R y x
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
left✝ : refl_trans_clos R x z
right✝ : refl_trans_clos R y z
⊢ joins R y x