intros le x y refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
R' : A → A → Prop
⊢ (fun R R' => ∀ (x y : A), R x y → R' x y) R R' →
    (fun R R' => ∀ (x y : A), R x y → R' x y) (refl_clos R) (refl_clos R')
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
R' : A → A → Prop
le : ∀ (x y : A), R x y → R' x y
x y : A
refl : refl_clos R x y
⊢ refl_clos R' x y