Apply unknownprop_f8cb4609f9c174a593de5a10197e2915f5c1a2d9f32ed8d30c3d30b788bb9e1e with λ x0 x1 : ι → ι → ι . ∀ x2 x3 x4 x5 . In (setsum x4 x5) (x1 x2 x3) ⟶ In x4 x2.

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)).

Apply unknownprop_576918d9e5f208b0d4afcf7c46d767aab50123519e7ada8ee8e8d0a4883e6b6c with x0, λ x4 . x1, x2, x3.

The subproof is completed by applying H0.

■

Proofgold Proof