intros x y z y1 red_x_y1 red_y1_y
case a.a
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 x_1 : A),
    refl_trans_clos R x x_1 →
      refl_trans_clos S x_1 y →
        ∀ (x_2 : A),
          refl_trans_clos R x x_2 →
            refl_trans_clos S x_2 z →
              ∃ 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
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
⊢ ∀ (x_1 : A),
    refl_trans_clos R x x_1 →
      refl_trans_clos S x_1 z →
        ∃ 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