cases rc
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✝
case a.step.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝ c✝ : A
step : trans_clos (refl_clos R) a✝ c✝
ih : refl_clos (trans_clos R) a✝ c✝
⊢ refl_clos (trans_clos R) a✝ c✝

case a.step.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y a✝¹ b✝ c✝ : A
step : trans_clos (refl_clos R) b✝ c✝
ih : refl_clos (trans_clos R) b✝ c✝
a✝ : R a✝¹ b✝
⊢ refl_clos (trans_clos R) a✝¹ c✝