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