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