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 (setexp x10 x8) (λ x12 x13 . ∀ x14 . x14 ∈ x8 ⟶ ∀ x15 . x15 ∈ x8 ⟶ x9 x14 x15 ⟶ x11 (ap x12 x14) (ap x13 x15))) x6 x7)) x0 x1) = (λ x4 . λ x5 : ι → ι → ο . λ x6 . λ x7 : ι → ι → ο . unpack_r_i (pack_r x4 x5) ((λ x8 . λ x9 : ι → ι → ο . λ x10 . λ x11 : ι → ι → ο . pack_r (setexp x10 x8) (λ x12 x13 . ∀ x14 . x14 ∈ x8 ⟶ ∀ x15 . x15 ∈ x8 ⟶ x9 x14 x15 ⟶ x11 (ap x12 x14) (ap x13 x15))) 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 (setexp x10 x8) (λ x12 x13 . ∀ x14 . ... ⟶ ∀ x15 . ... ⟶ x9 x14 x15 ⟶ x11 (ap x12 x14) (ap x13 x15))) ... ...)) ... ...,
...,
....
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 (setexp x10 x8) (λ x12 x13 . ∀ x14 . x14 ∈ x8 ⟶ ∀ x15 . x15 ∈ x8 ⟶ x9 x14 x15 ⟶ x11 (ap x12 x14) (ap x13 x15))) x6 x7)) x2 x3)set y5 to be
(λ x5 . λ x6 : ι → ι → ο . λ x7 . λ x8 : ι → ι → ο . pack_r (setexp x7 x5) (λ x9 x10 . ∀ x11 . x11 ∈ x5 ⟶ ∀ x12 . x12 ∈ x5 ⟶ x6 x11 x12 ⟶ x8 (ap x9 x11) (ap x10 x12))) 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 (setexp x9 x7) (λ x11 x12 . ∀ x13 . x13 ∈ x7 ⟶ ∀ x14 . x14 ∈ x7 ⟶ x8 x13 x14 ⟶ x10 (ap x11 x13) (ap x12 x14))) 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.