Theorem: refl_is_refl_trans (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
x y : A
⊢ refl_clos R x y → refl_trans_clos R x y
Tactic:
aesop
State after:
no goals