Let X, Y, rX, rY and f be given.
Set Phi to be the term
λX rX Y rY ⇒ f ∈ YX ∧ (∀x y ∈ X, rX x y → rY (f x) (f y)) of type
set → (set → set → prop) → set → (set → set → prop) → prop.
Set PhiX to be the term λX rX ⇒ unpack_r_o (pack_r Y rY) (λY' rY ⇒ Phi X rX Y' rY) of type set → (set → set → prop) → prop.
We will prove unpack_r_o (pack_r X rX) PhiX = Phi X rX Y rY.
We prove the intermediate
claim L1:
∀rX : set → set → prop, ∀rY' : set → set → prop, (∀x y ∈ Y, rY x y ↔ rY' x y) → Phi X rX Y rY' = Phi X rX Y rY.
Let rX be given.
Let rY' be given.
Assume HrY'.
Apply prop_ext_2 to the current goal.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We prove the intermediate
claim Lf:
∀x ∈ X, f x ∈ Y.
Let x be given.
An exact proof term for the current goal is ap_Pi X (λ_ ⇒ Y) f x H1.
We will
prove f ∈ YX ∧ (∀x y ∈ X, rX x y → rY (f x) (f y)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy H7.
Apply iffER (rY (f x) (f y)) (rY' (f x) (f y)) (HrY' (f x) (Lf x Hx) (f y) (Lf y Hy)) to the current goal.
An exact proof term for the current goal is H2 x Hx y Hy H7.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We prove the intermediate
claim Lf:
∀x ∈ X, f x ∈ Y.
Let x be given.
An exact proof term for the current goal is ap_Pi X (λ_ ⇒ Y) f x H1.
We will
prove f ∈ YX ∧ (∀x y ∈ X, rX x y → rY' (f x) (f y)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy H7.
Apply iffEL (rY (f x) (f y)) (rY' (f x) (f y)) (HrY' (f x) (Lf x Hx) (f y) (Lf y Hy)) to the current goal.
An exact proof term for the current goal is H2 x Hx y Hy H7.
We prove the intermediate
claim L2:
∀rX' : set → set → prop, (∀x y ∈ X, rX x y ↔ rX' x y) → PhiX X rX' = PhiX X rX.
Let rX' be given.
Assume HrX'.
We will prove PhiX X rX' = PhiX X rX.
We will prove unpack_r_o (pack_r Y rY) (λY' rY ⇒ Phi X rX' Y' rY) = unpack_r_o (pack_r Y rY) (λY' rY ⇒ Phi X rX Y' rY).
Use transitivity with Phi X rX' Y rY, and Phi X rX Y rY.
We will prove unpack_r_o (pack_r Y rY) (Phi X rX') = Phi X rX' Y rY.
An exact proof term for the current goal is unpack_r_o_eq (Phi X rX') Y rY (L1 rX').
We will prove Phi X rX' Y rY = Phi X rX Y rY.
Apply prop_ext_2 to the current goal.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We will
prove f ∈ YX ∧ (∀x y ∈ X, rX x y → rY (f x) (f y)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy H7.
Apply H2 x Hx y Hy to the current goal.
Apply iffEL (rX x y) (rX' x y) (HrX' x Hx y Hy) to the current goal.
An exact proof term for the current goal is H7.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We will
prove f ∈ YX ∧ (∀x y ∈ X, rX' x y → rY (f x) (f y)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
Let y be given.
Assume Hy H7.
Apply H2 x Hx y Hy to the current goal.
Apply iffER (rX x y) (rX' x y) (HrX' x Hx y Hy) to the current goal.
An exact proof term for the current goal is H7.
Use symmetry.
An exact proof term for the current goal is unpack_r_o_eq (Phi X rX) Y rY (L1 rX).
Use transitivity with and PhiX X rX.
An exact proof term for the current goal is unpack_r_o_eq PhiX X rX L2.
We will prove unpack_r_o (pack_r Y rY) (Phi X rX) = Phi X rX Y rY.
An exact proof term for the current goal is unpack_r_o_eq (Phi X rX) Y rY (L1 rX).