Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: nIn x2 2.

Apply unknownprop_fe7ff313be3d0b9f2334c12982636aff94f7603137e8053506a95c79965309c2 with ap (setsum x0 x1) x2.

Let x3 of type ι be given.

Apply unknownprop_b30a94f49240f0717f4ecb200a605aa8a4e6dad6dc5d1afa60c37866ee96baab with x3, ap (setsum x0 x1) x2.

Assume H1: In x3 (ap (setsum x0 x1) x2).

Claim L2: In (setsum x2 x3) (setsum x0 x1)

Apply unknownprop_762358d061bd2484ba81471a0b72cf827e125ecce5f1471d9abb4ee5039695f2 with setsum x0 x1, x2, x3.

The subproof is completed by applying H1.

Apply unknownprop_eb8e8f72a91f1b934993d4cb19c84c8270f73a3626f3022b683d960a7fef89cb with ∃ x4 . and (In x4 x0) (setsum x2 x3 = setsum 0 x4), ∃ x4 . and (In x4 x1) (setsum x2 x3 = setsum 1 x4), False leaving 3 subgoals.

Apply unknownprop_c529973cb32f8d02a3950eda53e547d40c4a0e8faca1777353233a3377534f09 with x0, x1, setsum x2 x3.

The subproof is completed by applying L2.

Assume H3: ∃ x4 . and (In x4 x0) (setsum x2 x3 = setsum 0 x4).

Apply unknownprop_3848cfb1fd522cb609408da39f227a9c05924a24919f21041d0880590b824ef5 with λ x4 . In x4 x0, λ x4 . setsum x2 x3 = setsum 0 x4, False leaving 2 subgoals.

The subproof is completed by applying H3.

Let x4 of type ι be given.

Assume H4: In x4 x0.

Assume H5: setsum x2 x3 = setsum 0 x4.

Apply unknownprop_8369708f37c0d20e10b6156293f1b207e835dfc563ff7fbfa059bf26c84ddb80 with x2, 2 leaving 2 subgoals.

The subproof is completed by applying H0.

Apply unknownprop_c29e201c2636d12615b11e1220001fcc0c2bbdeb53735eb34683c60a05a28860 with x2 = 0, x3 = x4, λ x5 x6 . In x6 2 leaving 2 subgoals.

Apply unknownprop_fafba38828754510d238125ccabe4414010fab04b5feedcfb4fb3ed8bfbb804e with x2, x3, 0, x4.

The subproof is completed by applying H5.

The subproof is completed by applying unknownprop_7630054952f4bd54be6e25e2e786a4db7b90ee782d6b1031afa63aeb6d55b595.

Assume H3: ∃ x4 . and (In x4 x1) (setsum x2 x3 = setsum 1 x4).

Apply unknownprop_3848cfb1fd522cb609408da39f227a9c05924a24919f21041d0880590b824ef5 with λ x4 . In x4 x1, λ x4 . setsum x2 x3 = setsum 1 x4, False leaving 2 subgoals.

The subproof is completed by applying H3.

Let x4 of type ι be given.

Assume H4: In x4 x1.

Assume H5: setsum x2 x3 = setsum 1 x4.

Apply unknownprop_8369708f37c0d20e10b6156293f1b207e835dfc563ff7fbfa059bf26c84ddb80 with x2, 2 leaving 2 subgoals.

The subproof is completed by applying H0.

Apply unknownprop_c29e201c2636d12615b11e1220001fcc0c2bbdeb53735eb34683c60a05a28860 with x2 = 1, x3 = x4, λ x5 x6 . In x6 2 leaving 2 subgoals.

Apply unknownprop_fafba38828754510d238125ccabe4414010fab04b5feedcfb4fb3ed8bfbb804e with x2, x3, 1, x4.

The subproof is completed by applying H5.

The subproof is completed by applying unknownprop_85e7394990c25c8874e39b4ca1ac83bc7d22390df4a86e0ba0fa73d0ca7d5d30.

■

Proofgold Proof