Let x0 of type ι be given.

Assume H0: nat_p x0.

Let x1 of type ι be given.

Assume H1: nat_p x1.

Apply unknownprop_4b95783dcb3eee1943e1de5542f675166ef402c8fbdda80bdf0920b55d3fc6de with setsum x0 x1, add_nat x0 x1, combine_funcs x0 x1 (λ x2 . x2) (λ x2 . add_nat x0 x2).

Apply unknownprop_aa42ade5598d8612d2029318c4ed81646c550ecc6cdd9ab953ce4bf73f3dd562 with setsum x0 x1, add_nat x0 x1, combine_funcs x0 x1 (λ x2 . x2) (λ x2 . add_nat x0 x2) leaving 2 subgoals.

Apply unknownprop_57c8600e4bc6abecef2ae17962906fa2de1fc16f5d46ed100ff99cd5b67f5b1b with setsum x0 x1, add_nat x0 x1, combine_funcs x0 x1 (λ x2 . x2) (λ x2 . add_nat x0 x2) leaving 2 subgoals.

Let x2 of type ι be given.

Assume H2: In x2 (setsum x0 x1).

Apply unknownprop_18583690a94a3aabb1b201c712283c6f832bd4e90b0730d0c8623d2e4a7a992a with x0, x1, x2, λ x3 . In (combine_funcs x0 x1 (λ x4 . x4) (λ x4 . add_nat x0 x4) x3) (add_nat x0 x1) leaving 3 subgoals.

The subproof is completed by applying H2.

Let x3 of type ι be given.

Assume H3: In x3 x0.

Apply unknownprop_d8973abfc5fd9b1197675b2a0610f261f9be335ec7d31dfa5c6a8b518bd2b06a with x0, x1, λ x4 . x4, λ x4 . add_nat x0 x4, x3, λ x4 x5 . In x5 (add_nat x0 x1).

Claim L4: Subq x0 (add_nat x0 x1)

Apply unknownprop_b206a252a4dfa00974a54a55a5d4cb4e0855569e1688fcc8ab9156674c2020fc with x0, x1.

The subproof is completed by applying H1.

Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with x0, add_nat x0 x1, x3 leaving 2 subgoals.

The subproof is completed by applying L4.

The subproof is completed by applying H3.

Let x3 of type ι be given.

Assume H3: In x3 x1.

Apply unknownprop_a6e435ff6762616eb80cd4cff726877e67d889d545b7ca4b4b9ea18c1b4ff1e8 with x0, x1, λ x4 . x4, λ x4 . add_nat x0 x4, x3, λ x4 x5 . In x5 (add_nat x0 x1).

Apply unknownprop_96cf1681687a72000e888b65b413651ac6a9efd1f56be6a7e59d74ac0cd27951 with x1, x3, x0 leaving 3 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H3.

The subproof is completed by applying H0.

Let x2 of type ι be given.

Assume H2: In x2 (setsum x0 x1).

Let x3 of type ι be given.

Assume H3: In x3 (setsum x0 x1).

Apply unknownprop_18583690a94a3aabb1b201c712283c6f832bd4e90b0730d0c8623d2e4a7a992a with x0, x1, x2, λ x4 . combine_funcs x0 x1 (λ x5 . x5) (λ x5 . add_nat x0 x5) x4 = combine_funcs x0 x1 (λ x5 . x5) (λ x5 . add_nat x0 x5) x3 ⟶ x4 = x3 leaving 3 subgoals.

The subproof is completed by applying H2.

Let x4 of type ι be given.

Assume H4: In x4 x0.

Apply unknownprop_d8973abfc5fd9b1197675b2a0610f261f9be335ec7d31dfa5c6a8b518bd2b06a with x0, x1, λ x5 . x5, λ x5 . add_nat x0 x5, x4, λ x5 x6 . x6 = combine_funcs x0 x1 (λ x7 . x7) (λ x7 . add_nat x0 x7) x3 ⟶ Inj0 x4 = x3.

Apply unknownprop_18583690a94a3aabb1b201c712283c6f832bd4e90b0730d0c8623d2e4a7a992a with x0, x1, x3, λ x5 . x4 = combine_funcs x0 x1 (λ x6 . x6) (λ x6 . add_nat x0 x6) x5 ⟶ Inj0 x4 = x5 leaving 3 subgoals.

The subproof is completed by applying H3.

Let x5 of type ι be given.

Assume H5: In x5 x0.

Apply unknownprop_d8973abfc5fd9b1197675b2a0610f261f9be335ec7d31dfa5c6a8b518bd2b06a with x0, x1, λ x6 . x6, λ x6 . add_nat x0 x6, x5, λ x6 x7 . x4 = x7 ⟶ Inj0 x4 = Inj0 x5.

Assume H6: x4 = (λ x6 . x6) x5.

Apply H6 with λ x6 x7 . Inj0 x7 = Inj0 x5.

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

Assume H7: x6 (Inj0 x5) (Inj0 x5).

The subproof is completed by applying H7.

Let x5 of type ι be given.

Assume H5: In x5 x1.

Apply unknownprop_a6e435ff6762616eb80cd4cff726877e67d889d545b7ca4b4b9ea18c1b4ff1e8 with x0, x1, λ x6 . ..., ..., ..., ....

...

■

Proofgold Proof