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.
set y11 to be ...
set y12 to be ...
Claim L2: ∀ x13 : ο → ο . x13 y12 ⟶ x13 y11
Let x13 of type ο → ο be given.
Assume H2:
x13 ((λ x14 . λ x15 x16 : ι → ι → ι . λ x17 x18 x19 . λ x20 x21 : ι → ι → ι . λ x22 x23 . and (and (and (and (y12 ∈ setexp x19 x14) (∀ x24 . x24 ∈ x14 ⟶ ∀ x25 . x25 ∈ x14 ⟶ ap y12 (x15 x24 x25) = x20 (ap y12 x24) (ap y12 x25))) (∀ x24 . x24 ∈ x14 ⟶ ∀ x25 . x25 ∈ x14 ⟶ ap y12 (x16 x24 x25) = x21 (ap y12 x24) (ap y12 x25))) (ap y12 x17 = x22)) (ap y12 x18 = x23)) x2 x4 x5 x8 x9 x3 x6 x7 x10 y11).
Apply unpack_b_b_e_e_o_eq with
λ x14 . λ x15 x16 : ι → ι → ι . λ x17 x18 . unpack_b_b_e_e_o (pack_b_b_e_e x3 x6 x7 x10 y11) (λ x19 . λ x20 x21 : ι → ι → ι . λ x22 x23 . (λ x24 . λ x25 x26 : ι → ι → ι . λ x27 x28 x29 . λ x30 x31 : ι → ι → ι . λ x32 x33 . and (and (and (and (y12 ∈ setexp x29 x24) (∀ x34 . x34 ∈ x24 ⟶ ∀ x35 . x35 ∈ x24 ⟶ ap y12 (x25 x34 x35) = x30 (ap y12 x34) (ap y12 x35))) (∀ x34 . x34 ∈ x24 ⟶ ∀ x35 . x35 ∈ x24 ⟶ ap y12 (x26 x34 x35) = x31 (ap y12 x34) (ap y12 x35))) (ap y12 x27 = x32)) (ap y12 x28 = x33)) x14 x15 x16 x17 x18 x19 x20 x21 x22 x23),
x2,
x4,
x5,
x8,
x9,
λ x14 : ο . x13 leaving 2 subgoals.
The subproof is completed by applying L1.
Apply unpack_b_b_e_e_o_eq with
(λ x14 . λ x15 x16 : ι → ι → ι . λ x17 x18 x19 . λ x20 x21 : ι → ι → ι . λ x22 x23 . and (and (and (and (y12 ∈ setexp x19 x14) (∀ x24 . x24 ∈ x14 ⟶ ∀ x25 . x25 ∈ x14 ⟶ ap y12 (x15 x24 x25) = x20 (ap y12 x24) (ap y12 x25))) (∀ x24 . x24 ∈ x14 ⟶ ∀ x25 . x25 ∈ x14 ⟶ ap y12 (x16 x24 x25) = x21 (ap y12 x24) (ap y12 x25))) (ap y12 x17 = x22)) (ap y12 x18 = x23)) x2 x4 ... ... ...,
...,
...,
...,
...,
...,
... leaving 2 subgoals.
Let x13 of type ο → ο → ο be given.
Apply L2 with
λ x14 : ο . x13 x14 y12 ⟶ x13 y12 x14.
Assume H3: x13 y12 y12.
The subproof is completed by applying H3.