. apply refl_trans_sym_refl_trans; trivial
case intro.intro.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y w : A
h1 : refl_trans_clos R w x
h2 : refl_trans_clos R w y
⊢ refl_trans_sym_clos R w y
no goals