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: nat_p x0.

Assume H1: nat_p x1.

Assume H2: equip x0 x2.

Assume H3: equip x1 x3.

Claim L4: ∀ x4 . nat_p x4 ⟶ ∀ x5 . equip x4 x5 ⟶ equip (add_nat x0 x4) (setsum x2 x5)

Apply nat_ind with λ x4 . ∀ x5 . equip x4 x5 ⟶ equip (add_nat x0 x4) (setsum x2 x5) leaving 2 subgoals.

Let x4 of type ι be given.

Assume H4: equip 0 x4.

Apply add_nat_0R with x0, λ x5 x6 . equip x6 (setsum x2 x4).

Apply unknownprop_b1ab55fb3adc1f5608875c7150ec0901fc5d8b2cbdf1e5df6d670947db1f7326 with x4, λ x5 x6 . equip x0 (setsum x2 x6) leaving 2 subgoals.

The subproof is completed by applying H4.

Apply equip_tra with x0, x2, setsum x2 0 leaving 2 subgoals.

The subproof is completed by applying H2.

Let x5 of type ο be given.

Assume H5: ∀ x6 : ι → ι . bij x2 (setsum x2 0) x6 ⟶ x5.

Apply H5 with Inj0.

Apply bijI with x2, setsum x2 0, Inj0 leaving 3 subgoals.

Let x6 of type ι be given.

Assume H6: x6 ∈ x2.

Apply Inj0_setsum with x2, 0, x6.

The subproof is completed by applying H6.

Let x6 of type ι be given.

Assume H6: x6 ∈ x2.

Let x7 of type ι be given.

Assume H7: x7 ∈ x2.

The subproof is completed by applying Inj0_inj with x6, x7.

Let x6 of type ι be given.

Assume H6: x6 ∈ setsum x2 0.

Apply setsum_Inj_inv with x2, 0, x6, ∃ x7 . and (x7 ∈ x2) (Inj0 x7 = x6) leaving 3 subgoals.

The subproof is completed by applying H6.

Assume H7: ∃ x7 . and (x7 ∈ x2) (x6 = Inj0 x7).

Apply H7 with ∃ x7 . and (x7 ∈ x2) (Inj0 x7 = x6).

Let x7 of type ι be given.

Assume H8: (λ x8 . and (x8 ∈ x2) (x6 = Inj0 x8)) x7.

Apply H8 with ∃ x8 . and (x8 ∈ x2) (Inj0 x8 = x6).

Assume H9: x7 ∈ x2.

Assume H10: x6 = Inj0 x7.

Let x8 of type ο be given.

Assume H11: ∀ x9 . and (x9 ∈ x2) (Inj0 x9 = x6) ⟶ x8.

Apply H11 with x7.

Apply andI with x7 ∈ x2, Inj0 x7 = x6 leaving 2 subgoals.

The subproof is completed by applying H9.

Let x9 of type ι → ι → ο be given.

The subproof is completed by applying H10 with λ x10 x11 . x9 x11 x10.

Assume H7: ∃ x7 . and (x7 ∈ 0) (x6 = Inj1 x7).

Apply H7 with ∃ x7 . and (x7 ∈ x2) (Inj0 x7 = x6).

Let x7 of type ι be given.

Assume H8: (λ x8 . and (x8 ∈ 0) (x6 = Inj1 x8)) x7.

Apply H8 with ∃ x8 . and (x8 ∈ x2) (Inj0 x8 = x6).

Assume H9: x7 ∈ 0.

Apply FalseE with x6 = Inj1 x7 ⟶ ∃ x8 . and (x8 ∈ x2) (Inj0 x8 = x6).

Apply EmptyE with x7.

The subproof is completed by applying H9.

Let x4 of type ι be given.

Assume H4: nat_p x4.

Assume H5: ∀ x5 . equip x4 x5 ⟶ equip (add_nat x0 x4) (setsum x2 x5).

Let x5 of type ι be given.

Assume H6: ....

...

Apply L4 with x1, x3 leaving 2 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H3.

■

Proofgold Proof