Theorem: equiv_conf
Proof state before:
case intro.intro
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
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ refl_trans_clos R y w ∧ refl_trans_clos R z w
Tactic:
constructor <;> apply refl_trans_clos_monotone
Proof state after:
case intro.intro.left.a
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
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ ∀ (x y : A), ?intro.intro.left.R x y → R x y

case intro.intro.left.a
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
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ refl_trans_clos ?intro.intro.left.R y w

case intro.intro.left.R
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
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ A → A → Prop

case intro.intro.right.a
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
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ ∀ (x y : A), ?intro.intro.right.R x y → R x y

case intro.intro.right.a
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
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ refl_trans_clos ?intro.intro.right.R z w

case intro.intro.right.R
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
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ A → A → Prop