. induction steps
  . constructor
  . apply refl_trans_clos_transitive
    . apply s_sub_r_star; trivial
    . trivial
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 mpr
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 R x y
⊢ refl_trans_clos S x y
case mpr
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 R x y
⊢ refl_trans_clos S x y