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