. cases hyp
  . aesop
  . apply trans_clos_monotone R <;> aesop
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
hyp : refl_clos (trans_clos R) x y
⊢ trans_clos (refl_clos R) x y

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