have h := semi x y z red_x_y red_x_z
case intro.intro.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
⊢ joins R y' z
case intro.intro.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
semi : semi_confluent R
x✝ w x y y' : A
red_x_y : R x y
_red_y_y' : refl_trans_clos R y y'
ih : ∀ (y_1 : A), refl_trans_clos R y y_1 → joins R y' y_1
z : A
red_x_z : refl_trans_clos R x z
h : joins R y z
⊢ joins R y' z