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 L0: ...

...

Claim L1: ∀ x5 : ι → ο . (∀ x6 . x6 ∈ x0 ⟶ iff (x2 x6) (x5 x6)) ⟶ (λ x6 . λ x7 : ι → ο . unpack_p_o (pack_p x1 x3) (λ x8 . λ x9 : ι → ο . (λ x10 . λ x11 : ι → ο . λ x12 . λ x13 : ι → ο . and (x4 ∈ setexp x12 x10) (∀ x14 . x14 ∈ x10 ⟶ x11 x14 ⟶ x13 (ap x4 x14))) x6 x7 x8 x9)) x0 x5 = (λ x6 . λ x7 : ι → ο . unpack_p_o (pack_p x1 x3) (λ x8 . λ x9 : ι → ο . (λ x10 . λ x11 : ι → ο . λ x12 . λ x13 : ι → ο . and (x4 ∈ setexp x12 x10) (∀ x14 . x14 ∈ x10 ⟶ x11 x14 ⟶ x13 (ap x4 x14))) x6 x7 x8 x9)) x0 x2

Let x5 of type ι → ο be given.

Assume H1: ∀ x6 . x6 ∈ x0 ⟶ iff (x2 x6) (x5 x6).

...

set y5 to be unpack_p_o (pack_p x0 x2) (λ x5 . λ x6 : ι → ο . unpack_p_o (pack_p x1 x3) (λ x7 . λ x8 : ι → ο . (λ x9 . λ x10 : ι → ο . λ x11 . λ x12 : ι → ο . and (x4 ∈ setexp x11 x9) (∀ x13 . x13 ∈ x9 ⟶ x10 x13 ⟶ x12 (ap x4 x13))) x5 x6 x7 x8))

set y6 to be (λ x6 . λ x7 : ι → ο . λ x8 . λ x9 : ι → ο . and (y5 ∈ setexp x8 x6) (∀ x10 . x10 ∈ x6 ⟶ x7 x10 ⟶ x9 (ap y5 x10))) x1 x3 x2 x4

Claim 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 . x12 ∈ x8 ⟶ x9 x12 ⟶ x11 (ap y6 x12))) x2 x4 x3 y5).

Apply unpack_p_o_eq with λ x8 . λ x9 : ι → ο . unpack_p_o (pack_p x3 y5) (λ x10 . λ x11 : ι → ο . (λ x12 . λ x13 : ι → ο . λ x14 . λ x15 : ι → ο . and (y6 ∈ setexp x14 x12) (∀ x16 . x16 ∈ x12 ⟶ x13 x16 ⟶ x15 (ap y6 x16))) x8 x9 x10 x11), x2, x4, λ x8 : ο . x7 leaving 2 subgoals.

The subproof is completed by applying L1.

Apply unpack_p_o_eq with (λ x8 . λ x9 : ι → ο . λ x10 . λ x11 : ι → ο . and (y6 ∈ setexp x10 x8) (∀ x12 . x12 ∈ x8 ⟶ x9 x12 ⟶ x11 (ap y6 x12))) 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.

■

Proofgold Proof