Let x0 of type ι be given.

Let x1 of type ι → ι be given.

Let x2 of type ι be given.

Apply unknownprop_a818f53272de918398012791887b763f90bf043f961a4f625d98076ca0b8b392 with In x2 (Pi x0 x1), 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 unknownprop_ca6c19086798ba340cae706688b2917b763d2e75dccd03c78c6b75434b998b10 with x0, x1, x2.

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

Apply andE with ∀ x3 . In x3 x2 ⟶ and (setsum_p x3) (In (ap x3 0) x0), ∀ x3 . In x3 x0 ⟶ In (ap x2 x3) (x1 x3), In x2 (Pi x0 x1) 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_1a1eed9c2e0652a509eabe7b8f07e31768cab0357ad1d97cb464202e3d371a17 with x0, x1, x2 leaving 2 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

■

Proofgold Proof