. apply diamond_implies_confluent
  simp [diamond]
  intros x y z y1 red_x_y1 red_y1_y
  intros z1 red_x_z1 red_z1_z
  have wedge_y1_z1 : wedge R y1 z1 :=
    by exists x
  have join_y1_z1 := conf_r _ _ wedge_y1_z1
  cases' join_y1_z1 with w h
  clear wedge_y1_z1
  have h1 := commut_r_s _ _ _ h.1 red_y1_y
  have h2 := commut_r_s _ _ _ h.2 red_z1_z
  cases' h1 with w1 h1
  cases' h2 with w2 h2
  have wedge_w1_w2 : wedge S w1 w2 :=
    by exists w; aesop
  have join_w1_w2 : joins S w1 w2 := by apply conf_s; trivial
  cases' join_w1_w2 with omega h3
  clear wedge_w1_w2
  exists omega; constructor
  . exists w1; aesop
  . exists w2; aesop
case 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
⊢ confluent fun x y => ∃ z, (fun x x_1 => refl_trans_clos R x x_1) x z ∧ (fun x x_1 => refl_trans_clos S x x_1) z y
no goals