induction' red_x_z with a x x₂ xₙ red_x_x2 red_x2_xn ih
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x z : A
red_x_z : refl_trans_clos R x z
⊢ ∀ (y : A), R x y → joins R y z
case a.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x z a : A
⊢ ∀ (y : A), R a y → joins R y a

case a.step
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), R x y → joins R y xₙ