intros x y red_x_y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ ∀ (x y : A), refl_trans_clos S x y → refl_trans_clos (fun x y => R x y ∨ S x y) x y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
x y : A
red_x_y : refl_trans_clos S x y
⊢ refl_trans_clos (fun x y => R x y ∨ S x y) x y