Let x0 of type ι be given.

Let x1 of type ι → ι be given.

Let x2 of type ι be given.

Assume H0: nIn x2 x0.

Apply unknownprop_fe7ff313be3d0b9f2334c12982636aff94f7603137e8053506a95c79965309c2 with ap (lam x0 (λ x3 . x1 x3)) x2.

Let x3 of type ι be given.

Apply unknownprop_b30a94f49240f0717f4ecb200a605aa8a4e6dad6dc5d1afa60c37866ee96baab with x3, ap (lam x0 (λ x4 . x1 x4)) x2.

Assume H1: In x3 (ap (lam x0 (λ x4 . x1 x4)) x2).

Claim L2: In (setsum x2 x3) (lam x0 (λ x4 . x1 x4))

Apply unknownprop_762358d061bd2484ba81471a0b72cf827e125ecce5f1471d9abb4ee5039695f2 with lam x0 (λ x4 . x1 x4), x2, x3.

The subproof is completed by applying H1.

Claim L3: In x2 x0

Apply unknownprop_576918d9e5f208b0d4afcf7c46d767aab50123519e7ada8ee8e8d0a4883e6b6c with x0, x1, x2, x3.

The subproof is completed by applying L2.

Apply unknownprop_8369708f37c0d20e10b6156293f1b207e835dfc563ff7fbfa059bf26c84ddb80 with x2, x0 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying L3.

■

Proofgold Proof