intros h y z x red_x_y red_y_z
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
⊢ (∀ (y z x : A),
      refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1) →
    ∀ (y z x : A),
      refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
⊢ ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1