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