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.

Let x5 of type ι be given.

Apply unknownprop_6e19704af9ad5218d3a56ceb94eb0641aa006b64f12b9d9f42f28f674bc7fda5 with x0, x1, x2, x3, x4, x5, 0, λ x6 x7 . x7 = binunion (binunion (f4b0e.. x0 x1 x2 x3) {(λ x9 . SetAdjoin x9 (Sing 5)) x8|x8 ∈ x4}) {(λ x9 . SetAdjoin x9 (Sing 6)) x8|x8 ∈ x5}.

Apply Repl_Empty with λ x6 . SetAdjoin x6 (Sing 7), λ x6 x7 . binunion (binunion (binunion (f4b0e.. x0 x1 x2 x3) {(λ x9 . SetAdjoin x9 (Sing 5)) x8|x8 ∈ x4}) {(λ x9 . SetAdjoin x9 (Sing 6)) x8|x8 ∈ x5}) x7 = binunion (binunion (f4b0e.. x0 x1 x2 x3) {(λ x9 . SetAdjoin x9 (Sing 5)) x8|x8 ∈ x4}) {(λ x9 . SetAdjoin x9 (Sing 6)) x8|x8 ∈ x5}.

Apply binunion_idr with binunion (binunion (f4b0e.. x0 x1 x2 x3) {(λ x7 . SetAdjoin x7 (Sing 5)) x6|x6 ∈ x4}) {(λ x7 . SetAdjoin x7 (Sing 6)) x6|x6 ∈ x5}, λ x6 x7 . x7 = binunion (binunion (f4b0e.. x0 x1 x2 x3) {(λ x9 . SetAdjoin x9 (Sing 5)) x8|x8 ∈ x4}) {(λ x9 . SetAdjoin x9 (Sing 6)) x8|x8 ∈ x5}.

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

Assume H0: x6 (binunion (binunion (f4b0e.. x0 x1 x2 x3) {(λ x8 . SetAdjoin x8 (Sing 5)) x7|x7 ∈ x4}) {(λ x8 . SetAdjoin x8 (Sing 6)) x7|x7 ∈ x5}) (binunion (binunion (f4b0e.. x0 x1 x2 x3) {(λ x8 . SetAdjoin x8 (Sing 5)) x7|x7 ∈ x4}) {(λ x8 . SetAdjoin x8 (Sing 6)) x7|x7 ∈ x5}).

The subproof is completed by applying H0.

■

Proofgold Proof