. apply refl_trans_clos_transitive <;> trivial
case mp.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : refl_trans_clos R a b
_red_b_c : refl_trans_clos (refl_trans_clos R) b c
ih : refl_trans_clos R b c
⊢ refl_trans_clos R a c

case mpr.refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y z : A
⊢ refl_trans_clos (refl_trans_clos R) z z

case mpr.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) a c
case mpr.refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y z : A
⊢ refl_trans_clos (refl_trans_clos R) z z

case mpr.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) a c