Let X, Y, opX, opY and f be given.
Set Phi to be the term
λX opX Y opY ⇒ f ∈ YX ∧ (∀x ∈ X, f (opX x) = opY (f x)) of type
set → (set → set) → set → (set → set) → prop.
Set PhiX to be the term λX opX ⇒ unpack_u_o (pack_u Y opY) (λY' opY ⇒ Phi X opX Y' opY) of type set → (set → set) → prop.
We will prove unpack_u_o (pack_u X opX) PhiX = Phi X opX Y opY.
We prove the intermediate
claim L1:
∀opX : set → set, ∀opY' : set → set, (∀x ∈ Y, opY x = opY' x) → Phi X opX Y opY' = Phi X opX Y opY.
Let opX be given.
Let opY' be given.
Assume HopY'.
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, f (opX x) = opY (f x)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
rewrite the current goal using HopY' (f x) (Lf x Hx) (from left to right).
An exact proof term for the current goal is H2 x Hx.
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, f (opX x) = opY' (f x)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
rewrite the current goal using HopY' (f x) (Lf x Hx) (from right to left).
An exact proof term for the current goal is H2 x Hx.
We prove the intermediate
claim L2:
∀opX' : set → set, (∀x ∈ X, opX x = opX' x) → PhiX X opX' = PhiX X opX.
Let opX' be given.
Assume HopX'.
We will prove PhiX X opX' = PhiX X opX.
We will prove unpack_u_o (pack_u Y opY) (λY' opY ⇒ Phi X opX' Y' opY) = unpack_u_o (pack_u Y opY) (λY' opY ⇒ Phi X opX Y' opY).
Use transitivity with Phi X opX' Y opY, and Phi X opX Y opY.
We will prove unpack_u_o (pack_u Y opY) (Phi X opX') = Phi X opX' Y opY.
An exact proof term for the current goal is unpack_u_o_eq (Phi X opX') Y opY (L1 opX').
We will prove Phi X opX' Y opY = Phi X opX Y opY.
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, f (opX x) = opY (f x)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
rewrite the current goal using HopX' x Hx (from left to right).
An exact proof term for the current goal is H2 x Hx.
Assume H.
Apply H to the current goal.
Assume H1 H2.
We will
prove f ∈ YX ∧ (∀x ∈ X, f (opX' x) = opY (f x)).
Apply andI to the current goal.
An exact proof term for the current goal is H1.
Let x be given.
Assume Hx.
rewrite the current goal using HopX' x Hx (from right to left).
An exact proof term for the current goal is H2 x Hx.
Use symmetry.
An exact proof term for the current goal is unpack_u_o_eq (Phi X opX) Y opY (L1 opX).
Use transitivity with and PhiX X opX.
An exact proof term for the current goal is unpack_u_o_eq PhiX X opX L2.
We will prove unpack_u_o (pack_u Y opY) (Phi X opX) = Phi X opX Y opY.
An exact proof term for the current goal is unpack_u_o_eq (Phi X opX) Y opY (L1 opX).