. apply (refl_trans_is_trans_refl _ _ _).2
  apply trans_clos_monotone
  . intros x y red
    apply  (refl_sym_is_sym_refl _ _ _).2
    trivial
  . trivial
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✝
no goals