. cases rc; trivial
  apply refl_clos.base; aesop
case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝ b✝ c✝ : A
rc : refl_clos R a✝ b✝
step : trans_clos (refl_clos R) b✝ c✝
ih : refl_clos (trans_clos R) b✝ c✝
⊢ refl_clos (trans_clos R) a✝ c✝
no goals