. induction' hyp with _ _ rc _ _ _ rc step ih
  . cases rc <;> aesop
  . cases rc; trivial
    apply refl_clos.base; aesop
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
no goals