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