Let x0 of type ι be given.

Let x1 of type ι → ι be given.

Let x2 of type ι be given.

Assume H0: In x2 (Pi x0 (λ x3 . x1 x3)).

Apply unknownprop_c20579f7ec03c9b411c1afcdcbd6eb7f887b4dea35b13dd2fe5a71172b6554fe with x0, x1, x2, and (∀ x3 . In x3 x2 ⟶ and (setsum_p x3) (In (ap x3 0) x0)) (∀ x3 . In x3 x0 ⟶ In (ap x2 x3) (x1 x3)) leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H1: ∀ x3 . In x3 x2 ⟶ and (setsum_p x3) (In (ap x3 0) x0).

Assume H2: ∀ x3 . In x3 x0 ⟶ In (ap x2 x3) (x1 x3).

Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with ∀ x3 . In x3 x2 ⟶ and (setsum_p x3) (In (ap x3 0) x0), ∀ x3 . In x3 x0 ⟶ In (ap x2 x3) (x1 x3) leaving 2 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

■

Proofgold Proof