simp
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (fun R R' => ∀ (x y : A), R x y → R' x y) (fun x x_1 => refl_trans_clos S x x_1)
    (refl_trans_clos ((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
⊢ ∀ (x y : A), refl_trans_clos S x y → refl_trans_clos (fun x y => R x y ∨ S x y) x y