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.

Let x5 of type ι be given.

Let x6 of type ι be given.

Let x7 of type ι be given.

Let x8 of type ι be given.

Assume H0: ∀ x9 . x9 ∈ x8 ⟶ ∀ x10 : ι → ο . x10 x0 ⟶ x10 x1 ⟶ x10 x2 ⟶ x10 x3 ⟶ x10 x4 ⟶ x10 x5 ⟶ x10 x6 ⟶ x10 x7 ⟶ x10 x9.

Let x9 of type ι be given.

Assume H1: x9 ⊆ x8.

Assume H2: atleastp 2 x9.

Let x10 of type ο be given.

Assume H3: x0 ∈ x9 ⟶ x1 ∈ x9 ⟶ x10.

Assume H4: x0 ∈ x9 ⟶ x2 ∈ x9 ⟶ x10.

Assume H5: x1 ∈ x9 ⟶ x2 ∈ x9 ⟶ x10.

Assume H6: x0 ∈ x9 ⟶ x3 ∈ x9 ⟶ x10.

Assume H7: x1 ∈ x9 ⟶ x3 ∈ x9 ⟶ x10.

Assume H8: x2 ∈ x9 ⟶ x3 ∈ x9 ⟶ x10.

Assume H9: x0 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10.

Assume H10: x1 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10.

Assume H11: x2 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10.

Assume H12: x3 ∈ x9 ⟶ x4 ∈ x9 ⟶ x10.

Assume H13: x0 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10.

Assume H14: x1 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10.

Assume H15: x2 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10.

Assume H16: x3 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10.

Assume H17: x4 ∈ x9 ⟶ x5 ∈ x9 ⟶ x10.

Assume H18: x0 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10.

Assume H19: x1 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10.

Assume H20: x2 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10.

Assume H21: x3 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10.

Assume H22: x4 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10.

Assume H23: x5 ∈ x9 ⟶ x6 ∈ x9 ⟶ x10.

Assume H24: x0 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10.

Assume H25: x1 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10.

Assume H26: x2 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10.

Assume H27: x3 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10.

Assume H28: x4 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10.

Assume H29: x5 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10.

Assume H30: x6 ∈ x9 ⟶ x7 ∈ x9 ⟶ x10.

Apply H2 with x10.

Let x11 of type ι → ι be given.

Assume H31: inj 2 x9 x11.

Apply H31 with x10.

Assume H32: ∀ x12 . x12 ∈ 2 ⟶ x11 x12 ∈ x9.

Assume H33: ∀ x12 . x12 ∈ 2 ⟶ ∀ x13 . x13 ∈ 2 ⟶ x11 x12 = x11 x13 ⟶ x12 = x13.

Apply H0 with x11 0, λ x12 . ... = ... ⟶ x10 leaving 10 subgoals.

...

■

Proofgold Proof