intros commut_r_s conf_r conf_s
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ commute R S → confluent R → confluent S → confluent ((fun R S x y => R x y ∨ S x y) R 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
⊢ confluent ((fun R S x y => R x y ∨ S x y) R S)