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.
Let x9 of type ι be given.
Let x10 of type ι be given.
Let x11 of type ι be given.
Let x12 of type ι be given.
set y13 to be ...
set y14 to be ...
Claim L2: ∀ x15 : ο → ο . x15 y14 ⟶ x15 y13
Let x15 of type ο → ο be given.
Assume H2:
x15 ((λ x16 . λ x17 x18 : ι → ι → ι . λ x19 : ι → ι → ο . λ x20 x21 x22 . λ x23 x24 : ι → ι → ι . λ x25 : ι → ι → ο . λ x26 x27 . and (and (and (and (and (y14 ∈ setexp x22 x16) (∀ x28 . x28 ∈ x16 ⟶ ∀ x29 . x29 ∈ x16 ⟶ ap y14 (x17 x28 x29) = x23 (ap y14 x28) (ap y14 x29))) (∀ x28 . x28 ∈ x16 ⟶ ∀ x29 . x29 ∈ x16 ⟶ ap y14 (x18 x28 x29) = x24 (ap y14 x28) (ap y14 x29))) (∀ x28 . x28 ∈ x16 ⟶ ∀ x29 . x29 ∈ x16 ⟶ x19 x28 x29 ⟶ x25 (ap y14 x28) (ap y14 x29))) (ap y14 x20 = x26)) (ap y14 x21 = x27)) x2 x4 x5 x8 x10 x11 x3 x6 x7 x9 x12 y13).
Apply unpack_b_b_r_e_e_o_eq with
λ x16 . λ x17 x18 : ι → ι → ι . λ x19 : ι → ι → ο . λ x20 x21 . unpack_b_b_r_e_e_o (pack_b_b_r_e_e x3 x6 x7 x9 x12 y13) (λ x22 . λ x23 x24 : ι → ι → ι . λ x25 : ι → ι → ο . λ x26 x27 . (λ x28 . λ x29 x30 : ι → ι → ι . λ x31 : ι → ι → ο . λ x32 x33 x34 . λ x35 x36 : ι → ι → ι . λ x37 : ι → ι → ο . λ x38 x39 . and (and (and (and (and (y14 ∈ setexp x34 x28) (∀ x40 . x40 ∈ x28 ⟶ ∀ x41 . x41 ∈ x28 ⟶ ap y14 (x29 x40 x41) = x35 (ap y14 x40) (ap y14 x41))) (∀ x40 . x40 ∈ x28 ⟶ ∀ x41 . x41 ∈ x28 ⟶ ap y14 (x30 x40 x41) = x36 (ap y14 x40) (ap y14 x41))) (∀ x40 . x40 ∈ x28 ⟶ ∀ x41 . x41 ∈ x28 ⟶ x31 x40 x41 ⟶ x37 (ap y14 x40) (ap y14 x41))) (ap y14 x32 = x38)) (ap y14 x33 = x39)) x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27),
x2,
x4,
x5,
x8,
x10,
x11,
λ x16 : ο . x15 leaving 2 subgoals.
The subproof is completed by applying L1.
Apply unpack_b_b_r_e_e_o_eq with
(λ x16 . λ x17 x18 : ι → ι → ι . λ x19 : ι → ι → ο . λ x20 x21 x22 . λ x23 x24 : ι → ι → ι . λ x25 : ι → ι → ο . λ x26 x27 . and (and (and (and (and (y14 ∈ setexp x22 x16) (∀ x28 . ... ⟶ ∀ x29 . ... ⟶ ap ... ... = ...)) ...) ...) ...) ...) ... ... ... ... ... ...,
...,
...,
...,
...,
...,
...,
... leaving 2 subgoals.
Let x15 of type ο → ο → ο be given.
Apply L2 with
λ x16 : ο . x15 x16 y14 ⟶ x15 y14 x16.
Assume H3: x15 y14 y14.
The subproof is completed by applying H3.