apply refl_trans_union_left
case a.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 z : A
red_x_z : refl_trans_clos R x z
red_z_y : refl_trans_clos S z y
⊢ refl_trans_clos (fun x y => R x y ∨ S x y) x ?a.y✝
case a.a.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 z : A
red_x_z : refl_trans_clos R x z
red_z_y : refl_trans_clos S z y
⊢ refl_trans_clos (fun x y => R x y) x ?a.y✝