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 unknownprop_032e0e1ca2b6a6dec28f9022c0ab2a1eaf6a350eb9ef1a90bdd9222c65da37a1 with x0, x1, x2, x3, x4, 0, λ x5 x6 . x6 = binunion (f4b0e.. x0 x1 x2 x3) {(λ x8 . SetAdjoin x8 (Sing 5)) x7|x7 ∈ x4}.

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

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

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

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

The subproof is completed by applying H0.

■

Proofgold Proof