constructor
case refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y a✝ : A
⊢ refl_trans_sym_clos R a✝ a✝

case step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_sym_clos R b✝ c✝
⊢ refl_trans_sym_clos R a✝² c✝
case step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
R : A → A → Prop
x y a✝² b✝ c✝ : A
a✝¹ : R a✝² b✝
a✝ : refl_trans_clos R b✝ c✝
a_ih✝ : refl_trans_sym_clos R b✝ c✝
⊢ refl_trans_sym_clos R a✝² c✝