Claim L3:
∀ x0 . ∀ x1 : ι → ι → ο . ∀ x2 . ∀ x3 : ι → ι → ο . unpack_r_i (pack_r x2 x3) ((λ x4 . λ x5 : ι → ι → ο . λ x6 . λ x7 : ι → ι → ο . unpack_r_i (pack_r x4 x5) ((λ x8 . λ x9 : ι → ι → ο . λ x10 . λ x11 : ι → ι → ο . pack_r (setprod x8 x10) (λ x12 x13 . and (x9 (ap x12 0) (ap x13 0)) (x11 (ap x12 1) (ap x13 1)))) x6 x7)) x0 x1) = (λ x4 . λ x5 : ι → ι → ο . λ x6 . λ x7 : ι → ι → ο . unpack_r_i (pack_r x4 x5) ((λ x8 . λ x9 : ι → ι → ο . λ x10 . λ x11 : ι → ι → ο . pack_r (setprod x8 x10) (λ x12 x13 . and (x9 (ap x12 0) (ap x13 0)) (x11 (ap x12 1) (ap x13 1)))) x6 x7)) x0 x1 x2 x3Let x0 of type ι be given.
Let x1 of type ι → ι → ο be given.
Let x2 of type ι be given.
Let x3 of type ι → ι → ο be given.
Apply unpack_r_i_eq with
(λ x4 . λ x5 : ι → ι → ο . λ x6 . λ x7 : ι → ι → ο . unpack_r_i (pack_r x4 x5) ((λ x8 . λ x9 : ι → ι → ο . λ x10 . λ x11 : ι → ι → ο . pack_r (setprod x8 x10) (λ x12 x13 . and (x9 (ap x12 0) (ap x13 0)) (x11 (ap x12 1) (ap x13 1)))) x6 x7)) ... ...,
...,
....
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
unpack_r_i (pack_r x0 x1) ((λ x4 . λ x5 : ι → ι → ο . λ x6 . λ x7 : ι → ι → ο . unpack_r_i (pack_r x4 x5) ((λ x8 . λ x9 : ι → ι → ο . λ x10 . λ x11 : ι → ι → ο . pack_r (setprod x8 x10) (λ x12 x13 . and (x9 (ap x12 0) (ap x13 0)) (x11 (ap x12 1) (ap x13 1)))) x6 x7)) x2 x3)set y5 to be
(λ x5 . λ x6 : ι → ι → ο . λ x7 . λ x8 : ι → ι → ο . pack_r (setprod x5 x7) (λ x9 x10 . and (x6 (ap x9 0) (ap x10 0)) (x8 (ap x9 1) (ap x10 1)))) x1 x2 x3 y4Claim L4: ∀ x6 : ι → ο . x6 y5 ⟶ x6 y4
Let x6 of type ι → ο be given.
Assume H4:
x6 ((λ x7 . λ x8 : ι → ι → ο . λ x9 . λ x10 : ι → ι → ο . pack_r (setprod x7 x9) (λ x11 x12 . and (x8 (ap x11 0) (ap x12 0)) (x10 (ap x11 1) (ap x12 1)))) x2 x3 y4 y5).
Apply L3 with
y4,
y5,
x2,
x3,
λ x7 . x6.
Apply L1 with
x2,
x3,
y4,
y5,
λ x7 . x6.
The subproof is completed by applying H4.
Let x6 of type ι → ι → ο be given.
Apply L4 with
λ x7 . x6 x7 y5 ⟶ x6 y5 x7.
Assume H5: x6 y5 y5.
The subproof is completed by applying H5.