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_u_i (pack_u x0 x1) ((λ x6 . λ x7 : ι → ι . λ x8 . λ x9 : ι → ι . unpack_u_i (pack_u x6 x7) ((λ x10 . λ x11 : ι → ι . λ x12 . λ x13 : ι → ι . pack_u (setprod x10 x12) (λ x14 . lam 2 (λ x15 . If_i (x15 = 0) (x11 (ap x14 0)) (x13 (ap x14 1))))) x8 x9)) x2 x3))Let x5 of type ι → ο be given.
Assume H1:
x5 ((λ x6 . λ x7 : ι → ι . λ x8 . λ x9 : ι → ι . pack_u (setprod x6 x8) (λ x10 . lam 2 (λ x11 . If_i (x11 = 0) (x7 (ap x10 0)) (x9 (ap x10 1))))) x1 x2 x3 y4).
Apply unpack_u_i_eq with
(λ x6 . λ x7 : ι → ι . λ x8 . λ x9 : ι → ι . unpack_u_i (pack_u x6 x7) ((λ x10 . λ x11 : ι → ι . λ x12 . λ x13 : ι → ι . pack_u (setprod x10 x12) (λ x14 . lam 2 (λ x15 . If_i (x15 = 0) (x11 (ap x14 0)) (x13 (ap x14 1))))) x8 x9)) x3 y4,
x1,
x2,
λ x6 . x5 leaving 2 subgoals.
Let x6 of type ι → ι be given.
Assume H2: ∀ x7 . x7 ∈ x1 ⟶ x2 x7 = x6 x7.
Apply L0 with
x1,
x6,
x3,
y4,
λ x7 x8 . x8 = unpack_u_i (pack_u x3 y4) ((λ x9 . λ x10 : ι → ι . λ x11 . λ x12 : ι → ι . pack_u (setprod x9 x11) (λ x13 . lam 2 (λ x14 . If_i (x14 = 0) (x10 (ap x13 0)) (x12 (ap x13 1))))) x1 x2).
Apply L0 with
x1,
x2,
x3,
y4,
λ x7 x8 . (λ x9 . λ x10 : ι → ι . λ x11 . λ x12 : ι → ι . pack_u (setprod x9 x11) (λ x13 . lam 2 (λ x14 . If_i (x14 = 0) (x10 (ap x13 0)) (x12 (ap x13 1))))) x1 x6 x3 y4 = x8.
Apply pack_u_ext with
setprod x1 x3,
λ x7 . lam 2 (λ x8 . If_i (x8 = 0) (x6 (ap x7 0)) (y4 (ap x7 1))),
λ x7 . lam 2 (λ x8 . If_i (x8 = 0) (x2 (ap x7 0)) (y4 (ap x7 1))).
Let x7 of type ι be given.
Apply H2 with
ap x7 0,
λ x8 x9 . lam 2 (λ x10 . If_i (x10 = 0) (x6 ...) ...) = ... leaving 2 subgoals.
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.