Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι → ι be given.

Let x4 of type ι → ι be given.

Assume H0: inj x0 x2 x3.

Assume H1: inj x1 x2 x4.

Assume H2: ∀ x5 . In x5 x0 ⟶ ∀ x6 . In x6 x1 ⟶ not (x3 x5 = x4 x6).

Apply unknownprop_6a8f953ba7c3bf327e583b76a91b24ddd499843a498fbfe2514e26f3800e68b3 with x0, x2, x3, inj (setsum x0 x1) x2 (combine_funcs x0 x1 x3 x4) leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H3: ∀ x5 . In x5 x0 ⟶ In (x3 x5) x2.

Assume H4: ∀ x5 . In x5 x0 ⟶ ∀ x6 . In x6 x0 ⟶ x3 x5 = x3 x6 ⟶ x5 = x6.

Apply unknownprop_6a8f953ba7c3bf327e583b76a91b24ddd499843a498fbfe2514e26f3800e68b3 with x1, x2, x4, inj (setsum x0 x1) x2 (combine_funcs x0 x1 x3 x4) leaving 2 subgoals.

The subproof is completed by applying H1.

Assume H5: ∀ x5 . In x5 x1 ⟶ In (x4 x5) x2.

Assume H6: ∀ x5 . In x5 x1 ⟶ ∀ x6 . In x6 x1 ⟶ x4 x5 = x4 x6 ⟶ x5 = x6.

Apply unknownprop_57c8600e4bc6abecef2ae17962906fa2de1fc16f5d46ed100ff99cd5b67f5b1b with setsum x0 x1, x2, combine_funcs x0 x1 x3 x4 leaving 2 subgoals.

Let x5 of type ι be given.

Assume H7: In x5 (setsum x0 x1).

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

The subproof is completed by applying H7.

Let x6 of type ι be given.

Assume H8: In x6 x0.

Apply unknownprop_d8973abfc5fd9b1197675b2a0610f261f9be335ec7d31dfa5c6a8b518bd2b06a with x0, x1, x3, x4, x6, λ x7 x8 . In x8 x2.

Apply H3 with x6.

The subproof is completed by applying H8.

Let x6 of type ι be given.

Assume H8: In x6 x1.

Apply unknownprop_a6e435ff6762616eb80cd4cff726877e67d889d545b7ca4b4b9ea18c1b4ff1e8 with x0, x1, x3, x4, x6, λ x7 x8 . In x8 x2.

Apply H5 with x6.

The subproof is completed by applying H8.

Let x5 of type ι be given.

Assume H7: In x5 (setsum x0 x1).

Let x6 of type ι be given.

Assume H8: In x6 (setsum x0 x1).

Apply unknownprop_18583690a94a3aabb1b201c712283c6f832bd4e90b0730d0c8623d2e4a7a992a with x0, x1, x5, λ x7 . combine_funcs x0 x1 x3 x4 x7 = combine_funcs x0 x1 x3 x4 x6 ⟶ x7 = x6 leaving 3 subgoals.

The subproof is completed by applying H7.

Let x7 of type ι be given.

Assume H9: In x7 x0.

Apply unknownprop_d8973abfc5fd9b1197675b2a0610f261f9be335ec7d31dfa5c6a8b518bd2b06a with x0, x1, x3, x4, x7, λ x8 x9 . x9 = combine_funcs x0 x1 x3 x4 x6 ⟶ Inj0 x7 = x6.

Apply unknownprop_18583690a94a3aabb1b201c712283c6f832bd4e90b0730d0c8623d2e4a7a992a with x0, x1, x6, λ x8 . x3 x7 = combine_funcs x0 x1 x3 x4 x8 ⟶ Inj0 x7 = x8 leaving 3 subgoals.

The subproof is completed by applying H8.

Let x8 of type ι be given.

Assume H10: In x8 x0.

Apply unknownprop_d8973abfc5fd9b1197675b2a0610f261f9be335ec7d31dfa5c6a8b518bd2b06a with x0, x1, x3, x4, x8, λ x9 x10 . x3 x7 = x10 ⟶ Inj0 x7 = Inj0 x8.

Assume H11: x3 x7 = x3 x8.

Apply H4 with x7, x8, λ x9 x10 . Inj0 x10 = Inj0 x8 leaving 4 subgoals.

The subproof is completed by applying H9.

The subproof is completed by applying H10.

The subproof is completed by applying H11.

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

Assume H12: x9 (Inj0 x8) (Inj0 x8).

The subproof is completed by applying H12.

...

■

Proofgold Proof