exists w
case a.step.intro.base.intro
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
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ joins R y xₙ
case a.step.intro.base.intro
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
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R y w ∧ refl_trans_clos R xₙ w