. apply h.1
case a.step.intro.refl.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
h : refl_trans_clos R y x₂ ∧ refl_clos R x₂ x₂
⊢ refl_trans_clos R y ?a.step.intro.refl.left.y✝

case a.step.intro.refl.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
h : refl_trans_clos R y x₂ ∧ refl_clos R x₂ x₂
⊢ refl_trans_clos R ?a.step.intro.refl.left.y✝ xₙ

case a.step.intro.refl.left.y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
h : refl_trans_clos R y x₂ ∧ refl_clos R x₂ x₂
⊢ A
case a.step.intro.refl.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
h : refl_trans_clos R y x₂ ∧ refl_clos R x₂ x₂
⊢ refl_trans_clos R x₂ xₙ