simp
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ ∀ (R : A → A → Prop),
    (fun R R' => ∀ (x y : A), R x y ↔ R' x y) (refl_trans_clos (refl_trans_clos R)) (refl_trans_clos R)
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ ∀ (R : A → A → Prop) (x y : A), refl_trans_clos (refl_trans_clos R) x y ↔ refl_trans_clos R x y