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_u_o (pack_u x1 x3) (λ x8 . λ x9 : ι → ι . (λ x10 . λ x11 : ι → ι . λ x12 . λ x13 : ι → ι . and (x4 ∈ setexp x12 x10) (∀ x14 . x14 ∈ x10 ⟶ ap x4 (x11 x14) = x13 (ap x4 x14))) x6 x7 x8 x9)) x0 x5 = (λ x6 . λ x7 : ι → ι . unpack_u_o (pack_u x1 x3) (λ x8 . λ x9 : ι → ι . (λ x10 . λ x11 : ι → ι . λ x12 . λ x13 : ι → ι . and (x4 ∈ setexp x12 x10) (∀ x14 . x14 ∈ x10 ⟶ ap x4 (x11 x14) = x13 (ap x4 x14))) x6 x7 x8 x9)) x0 x2set y5 to be
unpack_u_o (pack_u x0 x2) (λ x5 . λ x6 : ι → ι . unpack_u_o (pack_u x1 x3) (λ x7 . λ x8 : ι → ι . (λ x9 . λ x10 : ι → ι . λ x11 . λ x12 : ι → ι . and (x4 ∈ setexp x11 x9) (∀ x13 . x13 ∈ x9 ⟶ ap x4 (x10 x13) = x12 (ap x4 x13))) x5 x6 x7 x8))set y6 to be
(λ x6 . λ x7 : ι → ι . λ x8 . λ x9 : ι → ι . and (y5 ∈ setexp x8 x6) (∀ x10 . x10 ∈ x6 ⟶ ap y5 (x7 x10) = x9 (ap y5 x10))) 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 ⟶ ap y6 (x9 x12) = x11 (ap y6 x12))) x2 x4 x3 y5).
Apply unpack_u_o_eq with
λ x8 . λ x9 : ι → ι . unpack_u_o (pack_u x3 y5) (λ x10 . λ x11 : ι → ι . (λ x12 . λ x13 : ι → ι . λ x14 . λ x15 : ι → ι . and (y6 ∈ setexp x14 x12) (∀ x16 . x16 ∈ x12 ⟶ ap y6 (x13 x16) = x15 (ap y6 x16))) x8 x9 x10 x11),
x2,
x4,
λ x8 : ο . x7 leaving 2 subgoals.
The subproof is completed by applying L1.
Apply unpack_u_o_eq with
(λ x8 . λ x9 : ι → ι . λ x10 . λ x11 : ι → ι . and (y6 ∈ setexp x10 x8) (∀ x12 . x12 ∈ x8 ⟶ ap y6 (x9 x12) = x11 (ap y6 x12))) 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.