have wedge_w1_w2 : wedge S w1 w2 :=
  by exists w; aesop
case a.a.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w
case a.a.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
wedge_w1_w2 : wedge S w1 w2
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w