Let x0 of type ι be given.
Let x1 of type ι → ι → ι be given.
Let x2 of type ι be given.
Let x3 of type ι → ι → ι be given.
set y4 to be ...
Claim L1:
∀ x5 : ι → ο . x5 y4 ⟶ x5 (unpack_b_i (pack_b x0 x1) ((λ x6 . λ x7 : ι → ι → ι . λ x8 . λ x9 : ι → ι → ι . unpack_b_i (pack_b x6 x7) ((λ x10 . λ x11 : ι → ι → ι . λ x12 . λ x13 : ι → ι → ι . pack_b (setprod x10 x12) (λ x14 x15 . lam 2 (λ x16 . If_i (x16 = 0) (x11 (ap x14 0) (ap x15 0)) (x13 (ap x14 1) (ap x15 1))))) x8 x9)) x2 x3))Let x5 of type ι → ο be given.
Assume H1:
x5 ((λ x6 . λ x7 : ι → ι → ι . λ x8 . λ x9 : ι → ι → ι . pack_b (setprod x6 x8) (λ x10 x11 . lam 2 (λ x12 . If_i (x12 = 0) (x7 (ap x10 0) (ap x11 0)) (x9 (ap x10 1) (ap x11 1))))) x1 x2 x3 y4).
Apply unpack_b_i_eq with
(λ x6 . λ x7 : ι → ι → ι . λ x8 . λ x9 : ι → ι → ι . unpack_b_i (pack_b x6 x7) ((λ x10 . λ x11 : ι → ι → ι . λ x12 . λ x13 : ι → ι → ι . pack_b (setprod x10 x12) (λ x14 x15 . lam 2 (λ x16 . If_i (x16 = 0) (x11 (ap x14 0) (ap x15 0)) (x13 (ap x14 1) (ap x15 1))))) x8 x9)) x3 y4,
x1,
x2,
λ x6 . x5 leaving 2 subgoals.
Let x6 of type ι → ι → ι be given.
Assume H2: ∀ x7 . x7 ∈ x1 ⟶ ∀ x8 . x8 ∈ x1 ⟶ x2 x7 x8 = x6 x7 x8.
Apply L0 with
x1,
x6,
x3,
y4,
λ x7 x8 . x8 = unpack_b_i (pack_b x3 y4) ((λ x9 . λ x10 : ι → ι → ι . λ x11 . λ x12 : ι → ι → ι . pack_b (setprod x9 x11) (λ x13 x14 . lam 2 (λ x15 . If_i (x15 = 0) (x10 (ap x13 0) (ap x14 0)) (x12 (ap x13 1) (ap x14 1))))) x1 x2).
Apply L0 with
x1,
x2,
x3,
y4,
λ x7 x8 . (λ x9 . λ x10 : ι → ι → ι . λ x11 . λ x12 : ι → ι → ι . pack_b (setprod x9 x11) (λ x13 x14 . lam 2 (λ x15 . If_i (x15 = 0) (x10 (ap x13 0) (ap x14 0)) (x12 (ap x13 1) (ap x14 1))))) x1 x6 x3 y4 = x8.
Apply pack_b_ext with
setprod x1 x3,
λ x7 x8 . lam 2 (λ x9 . If_i (x9 = 0) (x6 (ap x7 0) ...) ...),
....
Let x5 of type ι → ι → ο be given.
Apply L1 with
λ x6 . x5 x6 y4 ⟶ x5 y4 x6.
Assume H2: x5 y4 y4.
The subproof is completed by applying H2.