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

Let x5 of type ι → ο be given.

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

set y6 to be ...

Apply unpack_r_i_eq with (λ x7 . λ x8 : ι → ι → ο . λ x9 . λ x10 : ι → ι → ο . unpack_r_i (pack_r x7 x8) ((λ x11 . λ x12 : ι → ι → ο . λ x13 . λ x14 : ι → ι → ο . pack_r (setsum x11 x13) (λ x15 x16 . or (and (and (x15 = Inj0 (Unj x15)) (x16 = Inj0 (Unj x16))) (x12 (Unj x15) (Unj x16))) (and (and (x15 = Inj1 (Unj x15)) (x16 = Inj1 (Unj x16))) (x14 (Unj x15) (Unj x16))))) x9 x10)) x3 y4, x1, y6, λ x7 . y6 leaving 2 subgoals.

Let x7 of type ι → ι → ο be given.

Assume H2: ∀ x8 . x8 ∈ x1 ⟶ ∀ x9 . x9 ∈ x1 ⟶ iff (y6 x8 x9) (x7 x8 x9).

Apply L0 with x1, x7, x3, y4, λ x8 x9 . x9 = unpack_r_i (pack_r x3 y4) ((λ x10 . λ x11 : ι → ι → ο . λ x12 . λ x13 : ι → ι → ο . pack_r (setsum x10 x12) (λ x14 x15 . or (and (and (x14 = Inj0 (Unj x14)) (x15 = Inj0 (Unj x15))) (x11 (Unj x14) (Unj x15))) (and (and (x14 = Inj1 (Unj x14)) (x15 = Inj1 (Unj x15))) (x13 (Unj x14) (Unj x15))))) x1 y6).

Apply L0 with x1, ..., ..., ..., ....

...

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