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

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_1675af88344c4eff7077f223dc9d7368946dad1693a26309b0fe16976c1762ed with x0, λ x4 . x1, x2, x3.

The subproof is completed by applying H0.

■

Proofgold Proof