Claim L0: ...

...

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_p_i (pack_p x0 x1) ((λ x6 . λ x7 : ι → ο . λ x8 . λ x9 : ι → ο . unpack_p_i (pack_p x6 x7) ((λ x10 . λ x11 : ι → ο . λ x12 . λ x13 : ι → ο . pack_p (setsum x10 x12) (λ x14 . or (and (x14 = Inj0 (Unj x14)) (x11 (Unj x14))) (and (x14 = Inj1 (Unj x14)) (x13 (Unj x14))))) x8 x9)) x2 x3))

Let x5 of type ι → ο be given.

Assume H1: x5 ((λ x6 . λ x7 : ι → ο . λ x8 . λ x9 : ι → ο . pack_p (setsum x6 x8) (λ x10 . or (and (x10 = Inj0 (Unj x10)) (x7 (Unj x10))) (and (x10 = Inj1 (Unj x10)) (x9 (Unj x10))))) x1 x2 x3 y4).

Apply unpack_p_i_eq with (λ x6 . λ x7 : ι → ο . λ x8 . λ x9 : ι → ο . unpack_p_i (pack_p x6 x7) ((λ x10 . λ x11 : ι → ο . λ x12 . λ x13 : ι → ο . pack_p (setsum x10 x12) (λ x14 . or (and (x14 = Inj0 (Unj x14)) (x11 (Unj x14))) (and (x14 = Inj1 (Unj x14)) (x13 (Unj x14))))) x8 x9)) x3 y4, x1, x2, λ x6 . x5 leaving 2 subgoals.

Let x6 of type ι → ο be given.

Assume H2: ∀ x7 . x7 ∈ x1 ⟶ iff (x2 x7) (x6 x7).

Apply L0 with x1, x6, x3, y4, λ x7 x8 . x8 = unpack_p_i (pack_p x3 y4) ((λ x9 . λ x10 : ι → ο . λ x11 . λ x12 : ι → ο . pack_p (setsum x9 x11) (λ x13 . or (and (x13 = Inj0 (Unj x13)) (x10 (Unj x13))) (and (x13 = Inj1 (Unj x13)) (x12 (Unj x13))))) x1 x2).

Apply L0 with x1, x2, x3, y4, λ x7 x8 . (λ x9 . λ x10 : ι → ο . λ x11 . λ x12 : ι → ο . pack_p (setsum x9 x11) (λ x13 . or (and (x13 = Inj0 (Unj x13)) (x10 (Unj x13))) (and (x13 = Inj1 (Unj x13)) (x12 (Unj x13))))) x1 x6 x3 y4 = x8.

Apply pack_p_ext with setsum x1 x3, λ x7 . or (and (x7 = Inj0 (Unj x7)) (x6 (Unj x7))) (and (x7 = Inj1 (Unj x7)) (y4 (Unj x7))), λ x7 . or (and (x7 = Inj0 (Unj x7)) (x2 (Unj x7))) ....

...

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.

■

Proofgold Proof