Let x0 of type ι be given.

Let x1 of type ι → ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H0: In (setsum x2 x3) (lam x0 (λ x4 . x1 x4)).

Apply unknownprop_e2d9dae0ea3a0bd6555cf6ae3b66e91e8730bfc402bf8dbafcc7b19c9adfb426 with x2, x3, λ x4 x5 . In x3 (x1 x4).

Apply unknownprop_d4bb68cbfba730ad1b1ee2c6901fadf3c573cb615fac3296f9bb52128e37668a with x2, x3, λ x4 x5 . In x4 (x1 (proj0 (setsum x2 x3))).

Apply unknownprop_90e3c298643df766b84b5eceef5956e9876cb7ac85576c91e0f6a929f73153ed with x0, x1, setsum x2 x3.

The subproof is completed by applying H0.

■

Proofgold Proof