. simp
  intros x y z red_x_z red_z_y
  apply refl_trans_clos_transitive
  . apply refl_trans_union_left
    trivial
  . apply refl_trans_union_right; trivial
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
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