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.

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

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

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

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

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

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

Claim L0: ∀ x7 : ι → ο . x7 y6 ⟶ x7 y5

Let x7 of type ι → ο be given.

Assume H0: x7 (binunion (UPair x2 x3) (binunion (binunion (Sing y6) (Sing x4)) (Sing y5))).

set y8 to be λ x8 . x7

Apply binunion_com with Sing x4, Sing y5, λ x9 x10 . binunion x10 (Sing y6) = binunion (binunion (Sing y6) (Sing x4)) (Sing y5), λ x9 x10 . y8 (binunion (UPair x2 x3) x9) (binunion (UPair x2 x3) x10) leaving 2 subgoals.

Apply binunion_asso with Sing y5, Sing x4, Sing y6, λ x9 x10 . x9 = binunion (binunion (Sing y6) (Sing x4)) (Sing y5).

Apply binunion_com with Sing x4, Sing y6, λ x9 x10 . binunion (Sing y5) x10 = binunion (binunion (Sing y6) (Sing x4)) (Sing y5).

The subproof is completed by applying binunion_com with Sing y5, binunion (Sing y6) (Sing x4).

The subproof is completed by applying H0.

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

Apply L0 with λ x8 . x7 x8 y6 ⟶ x7 y6 x8.

Assume H1: x7 y6 y6.

The subproof is completed by applying H1.

■

Proofgold Proof