Proofgold Proof

pf

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 x4 x0.

Apply unknownprop_5602d478ac2925d3761ba3ec5f78288f7907f59db6d1b15212dcf9b70f55d5f8 with x0, x1, setsum x2 x3.

The subproof is completed by applying H0.

■