. intros
  apply (refl_sym_is_sym_refl _ _ _).1
  trivial
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ ∀ (x y : A), ?a.R✝ x y → sym_clos (refl_clos R) x y

case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ trans_clos ?a.R✝ x✝ y✝

case a.R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ A → A → Prop
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x✝ y✝ : A
a✝ : refl_clos (trans_clos (sym_clos R)) x✝ y✝
⊢ trans_clos (fun x y => refl_clos (sym_clos R) x y) x✝ y✝