Let x0 of type ι be given.

Let x1 of type ι → ι be given.

Assume H0: ∀ x2 . In x2 x0 ⟶ In (x1 x2) (Power 1).

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

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

Let x2 of type ι be given.

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

Claim L2: x2 = 0

Apply unknownprop_fe7ff313be3d0b9f2334c12982636aff94f7603137e8053506a95c79965309c2 with x2.

Let x3 of type ι be given.

Apply unknownprop_b30a94f49240f0717f4ecb200a605aa8a4e6dad6dc5d1afa60c37866ee96baab with x3, x2.

Assume H2: In x3 x2.

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

The subproof is completed by applying H1.

Assume H3: ∀ x4 . In x4 x2 ⟶ and (setsum_p x4) (In (ap x4 0) x0).

Assume H4: ∀ x4 . In x4 x0 ⟶ In (ap x2 x4) (x1 x4).

Apply andE with setsum_p x3, In (ap x3 0) x0, False leaving 2 subgoals.

Apply H3 with x3.

The subproof is completed by applying H2.

Apply unknownprop_56bd0714abefd533b13603d171a24196c02fb0b6a0af8036287a8ec089f8957d with λ x4 x5 : ι → ο . x5 x3 ⟶ In (ap x3 0) x0 ⟶ False.

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

Assume H6: In (ap x3 0) x0.

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

Apply H4 with ap x3 0.

The subproof is completed by applying H6.

Claim L8: In (x1 (ap x3 0)) (Power 1)

Apply H0 with ap x3 0.

The subproof is completed by applying H6.

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

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

Apply unknownprop_b8811722bb772bba243207d8ee471ba24f8b88e821f7737307414168e638d2c6 with 1, x1 (ap x3 0).

The subproof is completed by applying L8.

The subproof is completed by applying L7.

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

Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with 1, Sing 0, ap x2 (ap x3 0) leaving 2 subgoals.

The subproof is completed by applying unknownprop_e8598561026ee5bf15479322ab1713bd41b786cd16638ceaff374ea0aee3dd94.

The subproof is completed by applying L9.

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

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

The subproof is completed by applying L10.

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

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

Apply H5 with λ x4 x5 . In x5 x2.

The subproof is completed by applying H2.

Claim L13: In (ap x3 1) 0

Apply L11 with λ x4 x5 . In (ap x3 1) x4.

The subproof is completed by applying L12.

Apply unknownprop_1cc88f7e87aaf8c5cee24b4a69ff535a81e7855c45a9fd971eec05ee4cc28f9c with ap x3 1.

The subproof is completed by applying L13.

Apply L2 with λ x3 x4 . In x4 1.

The subproof is completed by applying unknownprop_b28daf094ddd549776d741eec1dac894d28f0f162bae7bdbdbfb7366b31cdef0.

■

Proofgold Proof