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.
Assume H0: ∀ x8 : ι → ο . x8 x2 ⟶ x8 x3 ⟶ x8 x4 ⟶ x8 x5 ⟶ x8 x6 ⟶ x8 x7 ⟶ ∀ x9 . x0 x9 ⟶ x8 x9.
Assume H1: x0 x2.
Assume H2: x0 x3.
Assume H3: x0 x4.
Assume H4: x0 x5.
Assume H5: x0 x6.
Assume H6: x0 x7.
Assume H7: x1 x2.
Assume H8: x1 x3.
Assume H9: x1 x4.
Assume H10: x1 x5.
Let x8 of type ι → ι be given.
Let x9 of type ι → ι be given.
Let x10 of type ι → ι be given.
Assume H11: x8 x2 = x3.
Assume H12: x8 x3 = x2.
Assume H13: x8 x4 = x5.
Assume H14: x8 x5 = x4.
Assume H15: x9 x2 = x4.
Assume H16: x9 x3 = x5.
Assume H17: x9 x4 = x2.
Assume H18: x9 x5 = x3.
Assume H19: x10 x2 = x5.
Assume H20: x10 x3 = x4.
Assume H21: x10 x4 = x3.
Assume H22: x10 x5 = x2.
Let x11 of type ι → ι → ι → ι → ο be given.
Assume H23:
∀ x12 x13 . x0 x12 ⟶ x0 x13 ⟶ not (x11 x12 x13 x12 x13).
Assume H24: ∀ x12 x13 x14 x15 . x11 x12 x13 x14 x15 ⟶ x11 x14 x15 x12 x13.
Assume H25:
∀ x12 x13 . x0 x12 ⟶ x0 x13 ⟶ not (x11 x12 x13 x7 x7).
Assume H26:
∀ x12 x13 x14 x15 . x0 x12 ⟶ x1 x13 ⟶ x0 x14 ⟶ x1 x15 ⟶ not (x11 x12 x13 x14 x15) ⟶ not (x11 x12 (x8 x13) x14 (x8 x15)).
Assume H27:
∀ x12 x13 x14 x15 . x0 x12 ⟶ x1 x13 ⟶ x0 x14 ⟶ x1 x15 ⟶ not (x11 x12 x13 x14 x15) ⟶ not (x11 x12 (x9 x13) x14 (x9 x15)).
Assume H28:
∀ x12 x13 x14 x15 . x0 x12 ⟶ x1 x13 ⟶ x0 x14 ⟶ x1 x15 ⟶ not (x11 x12 x13 x14 x15) ⟶ not (x11 x12 (x10 x13) x14 (x10 x15)).
Assume H29:
∀ x12 . x0 x12 ⟶ not (x11 x4 x7 x5 x12).
Assume H30:
∀ x12 . x0 x12 ⟶ not (x11 x4 x7 x7 x12).
Assume H31:
∀ x12 . x0 x12 ⟶ not (x11 x5 x6 x6 x12).
Assume H32:
∀ x12 . x0 x12 ⟶ not (x11 x5 x7 x6 x12).
Assume H33:
∀ x12 . x0 x12 ⟶ not (x11 x6 x7 x4 x12).