. have h : R ∪ S ⊆ (. ~>₁* .) ∘ (. ~>₂* .) :=
    by
      simp; intros x y red_or
      cases red_or
      . exists y; aesop
      . exists x; aesop
  apply h
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
⊢ ∀ (x y : A), (fun x x_1 => (fun R S x y => R x y ∨ S x y) R S x x_1) x y → (fun x x_1 => ?S x x_1) x y

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
⊢ ∀ (x y : A),
    (fun x x_1 => ?S x x_1) x y → (fun x x_1 => refl_trans_clos ((fun R S x y => R x y ∨ S x y) R S) x x_1) x y

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 ?S

case S
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
⊢ A → A → Prop
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
⊢ ∀ (x y : A),
    (fun x x_1 => ∃ z, (fun x x_2 => refl_trans_clos R x x_2) x z ∧ (fun x x_2 => refl_trans_clos S x x_2) z x_1) x y →
      (fun x x_1 => refl_trans_clos ((fun R S x y => R x y ∨ S x y) R S) x x_1) x y

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