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.
Claim L1:
∀ x5 : (ι → ο) → ο . ... ⟶ (λ x6 . λ x7 : (ι → ο) → ο . unpack_c_o (pack_c x1 x3) (λ x8 . λ x9 : (ι → ο) → ο . (λ x10 . λ x11 : (ι → ο) → ο . λ x12 . λ x13 : (ι → ο) → ο . and (x4 ∈ setexp x12 x10) (∀ x14 : ι → ο . (∀ x15 . x14 x15 ⟶ x15 ∈ x12) ⟶ x13 x14 ⟶ x11 (λ x15 . and (x15 ∈ x10) (x14 (ap x4 x15))))) x6 x7 x8 x9)) x0 x5 = ...set y5 to be
unpack_c_o (pack_c x0 x2) (λ x5 . λ x6 : (ι → ο) → ο . unpack_c_o (pack_c x1 x3) (λ x7 . λ x8 : (ι → ο) → ο . (λ x9 . λ x10 : (ι → ο) → ο . λ x11 . λ x12 : (ι → ο) → ο . and (x4 ∈ setexp x11 x9) (∀ x13 : ι → ο . (∀ x14 . x13 x14 ⟶ x14 ∈ x11) ⟶ x12 x13 ⟶ x10 (λ x14 . and (x14 ∈ x9) (x13 (ap x4 x14))))) x5 x6 x7 x8))set y6 to be
(λ x6 . λ x7 : (ι → ο) → ο . λ x8 . λ x9 : (ι → ο) → ο . and (y5 ∈ setexp x8 x6) (∀ x10 : ι → ο . (∀ x11 . x10 x11 ⟶ x11 ∈ x8) ⟶ x9 x10 ⟶ x7 (λ x11 . and (x11 ∈ x6) (x10 (ap y5 x11))))) x1 x3 x2 x4Claim L2: ∀ x7 : ο → ο . x7 y6 ⟶ x7 y5
Let x7 of type ο → ο be given.
Assume H2:
x7 ((λ x8 . λ x9 : (ι → ο) → ο . λ x10 . λ x11 : (ι → ο) → ο . and (y6 ∈ setexp x10 x8) (∀ x12 : ι → ο . (∀ x13 . x12 x13 ⟶ x13 ∈ x10) ⟶ x11 x12 ⟶ x9 (λ x13 . and (x13 ∈ x8) (x12 (ap y6 x13))))) x2 x4 x3 y5).
Apply unpack_c_o_eq with
λ x8 . λ x9 : (ι → ο) → ο . unpack_c_o (pack_c x3 y5) (λ x10 . λ x11 : (ι → ο) → ο . (λ x12 . λ x13 : (ι → ο) → ο . λ x14 . λ x15 : (ι → ο) → ο . and (y6 ∈ setexp x14 x12) (∀ x16 : ι → ο . (∀ x17 . x16 x17 ⟶ x17 ∈ x14) ⟶ x15 x16 ⟶ x13 (λ x17 . and (x17 ∈ x12) (x16 (ap y6 x17))))) x8 x9 x10 x11),
x2,
x4,
λ x8 : ο . x7 leaving 2 subgoals.
The subproof is completed by applying L1.
Apply unpack_c_o_eq with
(λ x8 . λ x9 : (ι → ο) → ο . λ x10 . λ x11 : (ι → ο) → ο . and (y6 ∈ setexp x10 x8) (∀ x12 : ι → ο . (∀ x13 . x12 x13 ⟶ x13 ∈ x10) ⟶ x11 x12 ⟶ x9 (λ x13 . and (x13 ∈ x8) (x12 (ap y6 x13))))) x2 x4,
x3,
y5,
λ x8 : ο . x7 leaving 2 subgoals.
The subproof is completed by applying L0 with x4.
The subproof is completed by applying H2.
Let x7 of type ο → ο → ο be given.
Apply L2 with
λ x8 : ο . x7 x8 y6 ⟶ x7 y6 x8.
Assume H3: x7 y6 y6.
The subproof is completed by applying H3.