Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ι → ι be given.
Let x3 of type ι → ι → ι be given.
Let x4 of type ι be given.
Claim L1:
∀ x5 : ι → ι → ι . ... ⟶ (λ x6 . λ x7 : ι → ι → ι . unpack_b_o (pack_b x1 x3) (λ x8 . λ x9 : ι → ι → ι . (λ x10 . λ x11 : ι → ι → ι . λ x12 . λ x13 : ι → ι → ι . and (x4 ∈ setexp x12 x10) (∀ x14 . x14 ∈ x10 ⟶ ∀ x15 . x15 ∈ x10 ⟶ ap x4 (x11 x14 x15) = x13 (ap x4 x14) (ap x4 x15))) ... ... ... ...)) ... ... = ...set y5 to be
unpack_b_o (pack_b x0 x2) (λ x5 . λ x6 : ι → ι → ι . unpack_b_o (pack_b x1 x3) (λ x7 . λ x8 : ι → ι → ι . (λ x9 . λ x10 : ι → ι → ι . λ x11 . λ x12 : ι → ι → ι . and (x4 ∈ setexp x11 x9) (∀ x13 . x13 ∈ x9 ⟶ ∀ x14 . x14 ∈ x9 ⟶ ap x4 (x10 x13 x14) = x12 (ap x4 x13) (ap x4 x14))) x5 x6 x7 x8))set y6 to be
(λ x6 . λ x7 : ι → ι → ι . λ x8 . λ x9 : ι → ι → ι . and (y5 ∈ setexp x8 x6) (∀ x10 . x10 ∈ x6 ⟶ ∀ x11 . x11 ∈ x6 ⟶ ap y5 (x7 x10 x11) = x9 (ap y5 x10) (ap y5 x11))) x1 x3 x2 x4Claim L2: ∀ x7 : ο → ο . x7 y6 ⟶ x7 y5
Let x7 of type ο → ο be given.
Assume H2:
x7 ((λ x8 . λ x9 : ι → ι → ι . λ x10 . λ x11 : ι → ι → ι . and (y6 ∈ setexp x10 x8) (∀ x12 . x12 ∈ x8 ⟶ ∀ x13 . x13 ∈ x8 ⟶ ap y6 (x9 x12 x13) = x11 (ap y6 x12) (ap y6 x13))) x2 x4 x3 y5).
Apply unpack_b_o_eq with
λ x8 . λ x9 : ι → ι → ι . unpack_b_o (pack_b x3 y5) (λ x10 . λ x11 : ι → ι → ι . (λ x12 . λ x13 : ι → ι → ι . λ x14 . λ x15 : ι → ι → ι . and (y6 ∈ setexp x14 x12) (∀ x16 . x16 ∈ x12 ⟶ ∀ x17 . x17 ∈ x12 ⟶ ap y6 (x13 x16 x17) = x15 (ap y6 x16) (ap y6 x17))) x8 x9 x10 x11),
x2,
x4,
λ x8 : ο . x7 leaving 2 subgoals.
The subproof is completed by applying L1.
Apply unpack_b_o_eq with
(λ x8 . λ x9 : ι → ι → ι . λ x10 . λ x11 : ι → ι → ι . and (y6 ∈ setexp x10 x8) (∀ x12 . x12 ∈ x8 ⟶ ∀ x13 . x13 ∈ x8 ⟶ ap y6 (x9 x12 x13) = x11 (ap y6 x12) (ap y6 x13))) x2 x4,
x3,
y5,
λ x8 : ο . x7 leaving 2 subgoals.
The subproof is completed by applying L0 with x4.
The subproof is completed by applying H2.
Let x7 of type ο → ο → ο be given.
Apply L2 with
λ x8 : ο . x7 x8 y6 ⟶ x7 y6 x8.
Assume H3: x7 y6 y6.
The subproof is completed by applying H3.