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

Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: In x2 x0.

Let x3 of type ι be given.

Assume H1: In x3 x1.

Apply unknownprop_1633a25a08ee627a1613041ad1ebe0a4535d0c6ce109cb609e7d9a519dad2f25 with x0, λ x4 . x1, x2, x3 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

■

Proofgold Proof