Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Apply binunion_asso with UPair x0 x1, Sing x2, Sing x3, λ x4 x5 . x4 = binunion (binunion (UPair x0 x1) (Sing x3)) (Sing x2).

Apply binunion_asso with UPair x0 x1, Sing x3, Sing x2, λ x4 x5 . binunion (UPair x0 x1) (binunion (Sing x2) (Sing x3)) = x4.

set y4 to be binunion (UPair x0 x1) (binunion (Sing x2) (Sing x3))

set y5 to be binunion (UPair x1 x2) (binunion (Sing y4) (Sing x3))

Claim L0: ∀ x6 : ι → ο . x6 y5 ⟶ x6 y4

Let x6 of type ι → ο be given.

Assume H0: x6 (binunion (UPair x2 x3) (binunion (Sing y5) (Sing y4))).

set y7 to be λ x7 . x6

Apply binunion_com with Sing y4, Sing y5, λ x8 x9 . y7 (binunion (UPair x2 x3) x8) (binunion (UPair x2 x3) x9).

The subproof is completed by applying H0.

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

Apply L0 with λ x7 . x6 x7 y5 ⟶ x6 y5 x7.

Assume H1: x6 y5 y5.

The subproof is completed by applying H1.

■

Proofgold Proof