constructor
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (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),
      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
case mp
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (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),
      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

case mpr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (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) →
    ∀ (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