Let X, Y, pX, pY and f be given.
Set Phi to be the term
λX pX Y pY ⇒ f ∈ YX ∧ (∀x ∈ X, pX x → pY (f x)) of type
set → (set → prop) → set → (set → prop) → prop.
Set PhiX to be the term λX pX ⇒ unpack_p_o (pack_p Y pY) (λY' pY ⇒ Phi X pX Y' pY) of type set → (set → prop) → prop.
We will prove unpack_p_o (pack_p X pX) PhiX = Phi X pX Y pY.
We prove the intermediate
claim L1:
∀pX : set → prop, ∀pY' : set → prop, (∀x ∈ Y, pY x ↔ pY' x) → Phi X pX Y pY' = Phi X pX Y pY.
Let pX be given.
Let pY' be given.
Assume HpY'.
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 ∈ X, pX x → pY (f x)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx H7.
Apply iffER (pY (f x)) (pY' (f x)) (HpY' (f x) (Lf x Hx)) to the current goal.
An exact proof term for the current goal is H2 x Hx 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 ∈ X, pX x → pY' (f x)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx H7.
Apply iffEL (pY (f x)) (pY' (f x)) (HpY' (f x) (Lf x Hx)) to the current goal.
An exact proof term for the current goal is H2 x Hx H7.
We prove the intermediate
claim L2:
∀pX' : set → prop, (∀x ∈ X, pX x ↔ pX' x) → PhiX X pX' = PhiX X pX.
Let pX' be given.
Assume HpX'.
We will prove PhiX X pX' = PhiX X pX.
We will prove unpack_p_o (pack_p Y pY) (λY' pY ⇒ Phi X pX' Y' pY) = unpack_p_o (pack_p Y pY) (λY' pY ⇒ Phi X pX Y' pY).
Use transitivity with Phi X pX' Y pY, and Phi X pX Y pY.
We will prove unpack_p_o (pack_p Y pY) (Phi X pX') = Phi X pX' Y pY.
An exact proof term for the current goal is unpack_p_o_eq (Phi X pX') Y pY (L1 pX').
We will prove Phi X pX' Y pY = Phi X pX Y pY.
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 ∈ X, pX x → pY (f x)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx H7.
Apply H2 x Hx to the current goal.
Apply iffEL (pX x) (pX' x) (HpX' x Hx) 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 ∈ X, pX' x → pY (f x)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx H7.
Apply H2 x Hx to the current goal.
Apply iffER (pX x) (pX' x) (HpX' x Hx) 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_p_o_eq (Phi X pX) Y pY (L1 pX).
Use transitivity with and PhiX X pX.
An exact proof term for the current goal is unpack_p_o_eq PhiX X pX L2.
We will prove unpack_p_o (pack_p Y pY) (Phi X pX) = Phi X pX Y pY.
An exact proof term for the current goal is unpack_p_o_eq (Phi X pX) Y pY (L1 pX).