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.
Let x5 of type ι → ι → ι be given.
Let x6 of type ι be given.
Let x7 of type ι be given.
Let x8 of type ι be given.
set y9 to be ...
set y10 to be
(λ x10 . λ x11 x12 : ι → ι → ι . λ x13 x14 . λ x15 x16 : ι → ι → ι . λ x17 . and (and (and (y9 ∈ setexp x14 x10) (∀ x18 . ... ⟶ ∀ x19 . ... ⟶ ap y9 (x11 ... ...) = ...)) ...) ...) ... ... ... ... ... ... ... ...Claim L2: ∀ x11 : ο → ο . x11 y10 ⟶ x11 y9
Let x11 of type ο → ο be given.
Assume H2:
x11 ((λ x12 . λ x13 x14 : ι → ι → ι . λ x15 x16 . λ x17 x18 : ι → ι → ι . λ x19 . and (and (and (y10 ∈ setexp x16 x12) (∀ x20 . x20 ∈ x12 ⟶ ∀ x21 . x21 ∈ x12 ⟶ ap y10 (x13 x20 x21) = x17 (ap y10 x20) (ap y10 x21))) (∀ x20 . x20 ∈ x12 ⟶ ∀ x21 . x21 ∈ x12 ⟶ ap y10 (x14 x20 x21) = x18 (ap y10 x20) (ap y10 x21))) (ap y10 x15 = x19)) x2 x4 x5 x8 x3 x6 x7 y9).
Apply unpack_b_b_e_o_eq with
λ x12 . λ x13 x14 : ι → ι → ι . λ x15 . unpack_b_b_e_o (pack_b_b_e x3 x6 x7 y9) (λ x16 . λ x17 x18 : ι → ι → ι . λ x19 . (λ x20 . λ x21 x22 : ι → ι → ι . λ x23 x24 . λ x25 x26 : ι → ι → ι . λ x27 . and (and (and (y10 ∈ setexp x24 x20) (∀ x28 . x28 ∈ x20 ⟶ ∀ x29 . x29 ∈ x20 ⟶ ap y10 (x21 x28 x29) = x25 (ap y10 x28) (ap y10 x29))) (∀ x28 . x28 ∈ x20 ⟶ ∀ x29 . x29 ∈ x20 ⟶ ap y10 (x22 x28 x29) = x26 (ap y10 x28) (ap y10 x29))) (ap y10 x23 = x27)) x12 x13 x14 x15 x16 x17 x18 x19),
x2,
x4,
x5,
x8,
λ x12 : ο . x11 leaving 2 subgoals.
The subproof is completed by applying L1.
Apply unpack_b_b_e_o_eq with
(λ x12 . λ x13 x14 : ι → ι → ι . λ x15 x16 . λ x17 x18 : ι → ι → ι . λ x19 . and (and (and (y10 ∈ setexp x16 x12) (∀ x20 . x20 ∈ x12 ⟶ ∀ x21 . x21 ∈ x12 ⟶ ap y10 (x13 x20 x21) = x17 (ap y10 x20) (ap y10 x21))) (∀ x20 . x20 ∈ x12 ⟶ ∀ x21 . x21 ∈ x12 ⟶ ap y10 (x14 x20 x21) = x18 (ap y10 x20) (ap y10 x21))) (ap y10 x15 = x19)) x2 x4 x5 x8,
x3,
x6,
x7,
y9,
λ x12 : ο . x11 leaving 2 subgoals.
The subproof is completed by applying L0 with x4, x5.
The subproof is completed by applying H2.
Let x11 of type ο → ο → ο be given.
Apply L2 with
λ x12 : ο . x11 x12 y10 ⟶ x11 y10 x12.
Assume H3: x11 y10 y10.
The subproof is completed by applying H3.