Let x0 of type ι be given.

Let x1 of type ι → ι be given.

Assume H0: ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ prim4 1.

Apply PowerI with 1, Pi x0 (λ x2 . x1 x2).

Let x2 of type ι be given.

Assume H1: x2 ∈ Pi x0 (λ x3 . x1 x3).

Claim L2: x2 = 0

Apply Empty_eq with x2.

Let x3 of type ι be given.

Assume H2: x3 ∈ x2.

Apply PiE with x0, x1, x2, False leaving 2 subgoals.

The subproof is completed by applying H1.

Assume H3: ∀ x4 . x4 ∈ x2 ⟶ and (pair_p x4) (ap x4 0 ∈ x0).

Assume H4: ∀ x4 . x4 ∈ x0 ⟶ ap x2 x4 ∈ x1 x4.

Apply H3 with x3, False leaving 2 subgoals.

The subproof is completed by applying H2.

Assume H5: setsum (ap x3 0) (ap x3 1) = x3.

Assume H6: ap x3 0 ∈ x0.

Claim L7: ap x2 (ap x3 0) ∈ x1 (ap x3 0)

Apply H4 with ap x3 0.

The subproof is completed by applying H6.

Claim L8: x1 (ap x3 0) ∈ prim4 1

Apply H0 with ap x3 0.

The subproof is completed by applying H6.

Claim L9: ap x2 (ap x3 0) ∈ 1

Apply PowerE with 1, x1 (ap x3 0), ap x2 (ap x3 0) leaving 2 subgoals.

The subproof is completed by applying L8.

The subproof is completed by applying L7.

Claim L10: ap x2 (ap x3 0) ∈ Sing 0

Apply Subq_1_Sing0 with ap x2 (ap x3 0).

The subproof is completed by applying L9.

Claim L11: ap x2 (ap x3 0) = 0

Apply SingE with 0, ap x2 (ap x3 0).

The subproof is completed by applying L10.

Claim L12: ap x3 1 ∈ ap x2 (ap x3 0)

Apply apI with x2, ap x3 0, ap x3 1.

Apply H5 with λ x4 x5 . x5 ∈ x2.

The subproof is completed by applying H2.

Claim L13: ap x3 1 ∈ 0

Apply L11 with λ x4 x5 . ap x3 1 ∈ x4.

The subproof is completed by applying L12.

Apply EmptyE with ap x3 1.

The subproof is completed by applying L13.

Apply L2 with λ x3 x4 . x4 ∈ 1.

The subproof is completed by applying In_0_1.

■

Proofgold Proof