cases' joins_y_z with w h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : R x y
joins_y_z : joins R y z
⊢ joins R x z
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : A
red_x_y : R x y
w : A
h : refl_trans_clos R y w ∧ refl_trans_clos R z w
⊢ joins R x z