Let x0 of type ι be given.
Let x1 of type ι → ι → ι be given.
Assume H0:
∀ x2 . In x2 x0 ⟶ ∀ x3 . In x3 x0 ⟶ In (x1 x2 x3) x0.
Let x2 of type ι → ι → ι → ι be given.
Assume H1:
∀ x3 . In x3 x0 ⟶ ∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 x0 ⟶ In (x2 x3 x4 x5) x0.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι → ι → ι be given.
Assume H4:
∀ x6 . In x6 x0 ⟶ ∀ x7 . In x7 x0 ⟶ In (x5 x6 x7) x0.
Let x6 of type ι → ι → ι be given.
Assume H5:
∀ x7 . In x7 x0 ⟶ ∀ x8 . In x8 x0 ⟶ In (x6 x7 x8) x0.
Let x7 of type ι be given.
Let x8 of type ι → ι → ι be given.
Assume H7:
∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ In (x8 x9 x10) x0.
Assume H8:
∀ x9 . In x9 x0 ⟶ (x8 x7 x9 = x9 ⟶ False) ⟶ False.
Assume H9:
∀ x9 . In x9 x0 ⟶ (x8 x9 x7 = x9 ⟶ False) ⟶ False.
Assume H10:
∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ (x6 x9 (x8 x9 x10) = x10 ⟶ False) ⟶ False.
Assume H11:
∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ (x1 x9 x10 = x8 (x6 x9 x10) (x6 (x6 x9 x7) x7) ⟶ False) ⟶ False.
Assume H12:
∀ x9 . In x9 x0 ⟶ (x6 x7 x9 = x9 ⟶ False) ⟶ False.
Assume H13:
∀ x9 . In x9 x0 ⟶ (x6 x9 x9 = x7 ⟶ False) ⟶ False.
Assume H14:
∀ x9 . In x9 x0 ⟶ (x5 x7 x9 = x9 ⟶ False) ⟶ False.
Assume H15:
∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ (x2 x7 x9 x10 = x10 ⟶ False) ⟶ False.
Assume H16:
∀ x9 . In x9 x0 ⟶ ∀ x10 . In x10 x0 ⟶ (x2 x9 x7 x10 = x10 ⟶ False) ⟶ False.
Assume H17:
∀ x9 . ... ⟶ ∀ x10 . ... ⟶ ∀ x11 . ... ⟶ ∀ x12 . ... ⟶ (x2 x9 x11 (x5 x10 (x1 x9 (x2 x11 x10 (x2 x9 x11 (x5 x10 (x1 x9 (x2 x11 x10 (x2 x9 x11 (x5 x10 (x1 x9 (x2 x11 x10 (x2 ... ... ...)))))))))))) = ... ⟶ False) ⟶ False.