cases' h' with h1 h2
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y a✝¹ b✝ : A
a✝ : refl_trans_sym_clos R b✝ a✝¹
w : A
h' : refl_trans_clos R b✝ w ∧ refl_trans_clos R a✝¹ w
⊢ joins R a✝¹ b✝
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y a✝¹ b✝ : A
a✝ : refl_trans_sym_clos R b✝ a✝¹
w : A
h1 : refl_trans_clos R b✝ w
h2 : refl_trans_clos R a✝¹ w
⊢ joins R a✝¹ b✝