. aesop
case a.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x : A
⊢ trans_clos (refl_clos R) x x

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