cases' h1 with h11 h12
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
joins_y_z : joins R y z
w1 : A
h1 : refl_trans_clos R x w1 ∧ refl_trans_clos R y w1
⊢ joins R x z
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
joins_y_z : joins R y z
w1 : A
h11 : refl_trans_clos R x w1
h12 : refl_trans_clos R y w1
⊢ joins R x z