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