intros R x y
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
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y : A
⊢ refl_trans_clos (refl_trans_clos R) x y ↔ refl_trans_clos R x y