aesop
case a.step.base.a
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✝
⊢ trans_clos R a✝¹ c✝
no goals