induction steps
case mp
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y : A
steps : refl_trans_clos S x y
⊢ refl_trans_clos R x y
case mp.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝ : A
⊢ refl_trans_clos R a✝ a✝

case mp.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
r_sub_s : ∀ (x y : A), R x y → S x y
s_sub_r_star : ∀ (x y : A), S x y → refl_trans_clos R x y
x y a✝² b✝ c✝ : A
a✝¹ : S a✝² b✝
a✝ : refl_trans_clos S b✝ c✝
a_ih✝ : refl_trans_clos R b✝ c✝
⊢ refl_trans_clos R a✝² c✝