constructor <;> intros steps <;> induction' steps with z a b c red_a_c _red_b_c ih
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y : A
⊢ refl_trans_clos (refl_trans_clos R) x y ↔ refl_trans_clos R x y
case mp.refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y z : A
⊢ refl_trans_clos R z z

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