have h2 : refl_trans_clos (refl_trans_clos R) x z :=
  by
    apply (trans_clos_idempotent _ _ _).2; trivial
case mp
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos (refl_trans_clos R) x y →
      refl_trans_clos (refl_trans_clos R) x z →
        ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
h1 : refl_trans_clos (refl_trans_clos R) x y
⊢ ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
case mp
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
h :
  ∀ (y z x : A),
    refl_trans_clos (refl_trans_clos R) x y →
      refl_trans_clos (refl_trans_clos R) x z →
        ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_x_z : refl_trans_clos R x z
h1 : refl_trans_clos (refl_trans_clos R) x y
h2 : refl_trans_clos (refl_trans_clos R) x z
⊢ ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1