Let X, Y, CX, CY and f be given.
Set Phi to be the term λX CX Y CY ⇒ f ∈ YX ∧ (∀U : set → prop, (∀y, U y → y ∈ Y) → CY U → CX (λx ⇒ x ∈ X ∧ U (f x))) of type set → ((set → prop) → prop) → set → ((set → prop) → prop) → prop.
Set PhiX to be the term λX CX ⇒ unpack_c_o (pack_c Y CY) (λY' CY ⇒ Phi X CX Y' CY) of type set → ((set → prop) → prop) → prop.
We will prove unpack_c_o (pack_c X CX) PhiX = Phi X CX Y CY.
We prove the intermediate claim L1: ∀CX : (set → prop) → prop, ∀CY' : (set → prop) → prop, (∀U : set → prop, (∀y, U y → y ∈ Y) → (CY U ↔ CY' U)) → Phi X CX Y CY' = Phi X CX Y CY.
Let CX be given.
Let CY' be given.
Assume HCY'.
Apply prop_ext_2 to the current goal.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We will prove f ∈ YX ∧ (∀U : set → prop, (∀y, U y → y ∈ Y) → CY U → CX (λx ⇒ x ∈ X ∧ U (f x))).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let U be given.
Assume HU1 HU2.
We will prove CX (λx ⇒ x ∈ X ∧ U (f x)).
Apply H2 to the current goal.
An exact proof term for the current goal is HU1.
We will prove CY' U.
An exact proof term for the current goal is iffEL (CY U) (CY' U) (HCY' U HU1) HU2.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We will prove f ∈ YX ∧ (∀U : set → prop, (∀y, U y → y ∈ Y) → CY' U → CX (λx ⇒ x ∈ X ∧ U (f x))).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let U be given.
Assume HU1 HU2.
We will prove CX (λx ⇒ x ∈ X ∧ U (f x)).
Apply H2 to the current goal.
An exact proof term for the current goal is HU1.
We will prove CY U.
An exact proof term for the current goal is iffER (CY U) (CY' U) (HCY' U HU1) HU2.
We prove the intermediate claim L2: ∀CX' : (set → prop) → prop, (∀U : set → prop, (∀x, U x → x ∈ X) → (CX U ↔ CX' U)) → PhiX X CX' = PhiX X CX.
Let CX' be given.
Assume HCX'.
We will prove PhiX X CX' = PhiX X CX.
We will prove unpack_c_o (pack_c Y CY) (λY' CY ⇒ Phi X CX' Y' CY) = unpack_c_o (pack_c Y CY) (λY' CY ⇒ Phi X CX Y' CY).
Use transitivity with Phi X CX' Y CY, and Phi X CX Y CY.
We will prove unpack_c_o (pack_c Y CY) (Phi X CX') = Phi X CX' Y CY.
An exact proof term for the current goal is unpack_c_o_eq (Phi X CX') Y CY (L1 CX').
We will prove Phi X CX' Y CY = Phi X CX Y CY.
Apply prop_ext_2 to the current goal.
Assume H.
Apply H to the current goal.
Assume H1: f ∈ YX.
Assume H2: ∀U : set → prop, (∀y, U y → y ∈ Y) → CY U → CX' (λx ⇒ x ∈ X ∧ U (f x)).
We will prove f ∈ YX ∧ (∀U : set → prop, (∀y, U y → y ∈ Y) → CY U → CX (λx ⇒ x ∈ X ∧ U (f x))).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let U be given.
Assume HU1: ∀y, U y → y ∈ Y.
Assume HU2: CY U.
We prove the intermediate claim LU: ∀x, x ∈ X ∧ U (f x) → x ∈ X.
Let x be given.
An exact proof term for the current goal is andEL (x ∈ X) (U (f x)).
Apply iffER (CX (λx ⇒ x ∈ X ∧ U (f x))) (CX' (λx ⇒ x ∈ X ∧ U (f x))) (HCX' (λx ⇒ x ∈ X ∧ U (f x)) LU) to the current goal.
An exact proof term for the current goal is H2 U HU1 HU2.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We will prove f ∈ YX ∧ (∀U : set → prop, (∀y, U y → y ∈ Y) → CY U → CX' (λx ⇒ x ∈ X ∧ U (f x))).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let U be given.
Assume HU1: ∀y, U y → y ∈ Y.
Assume HU2: CY U.
We prove the intermediate claim LU: ∀x, x ∈ X ∧ U (f x) → x ∈ X.
Let x be given.
An exact proof term for the current goal is andEL (x ∈ X) (U (f x)).
Apply iffEL (CX (λx ⇒ x ∈ X ∧ U (f x))) (CX' (λx ⇒ x ∈ X ∧ U (f x))) (HCX' (λx ⇒ x ∈ X ∧ U (f x)) LU) to the current goal.
An exact proof term for the current goal is H2 U HU1 HU2.
Use symmetry.
An exact proof term for the current goal is unpack_c_o_eq (Phi X CX) Y CY (L1 CX).
Use transitivity with and PhiX X CX.
An exact proof term for the current goal is unpack_c_o_eq PhiX X CX L2.
We will prove unpack_c_o (pack_c Y CY) (Phi X CX) = Phi X CX Y CY.
An exact proof term for the current goal is unpack_c_o_eq (Phi X CX) Y CY (L1 CX).
∎