intros red
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
⊢ trans_clos R x y → refl_trans_clos R x y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y : A
red : trans_clos R x y
⊢ refl_trans_clos R x y