. intros y red_x_y
  cases' (str_conf _ _ _ red_x_y red_x_x2) with y₂ h
  cases h.2
  . exists xₙ; constructor
    . apply refl_trans_clos_transitive
      . apply h.1
      . trivial
    . constructor
  . have ih : y₂ ~>*.*<~ xₙ :=
      by apply ih; trivial
    cases' ih with w _
    exists w; constructor
    . apply refl_trans_clos_transitive
      . apply h.1
      . aesop
    . aesop
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ₙ
no goals