have join2 : y ~>*.*<~ w :=
by
  apply ih
  . apply trans_clos.base
    apply red_x_y'
  . aesop
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
⊢ joins R y z
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
join2 : joins R y w
⊢ joins R y z