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.
Let x9 of type ι → ι → ι be given.
Let x10 of type ι → ι → ι be given.
Let x11 of type ι → ι → ι be given.
Let x12 of type ι → ι → ι be given.
Let x13 of type ι → ι → ο be given.
Let x14 of type ι → ι → ι → ο be given.
Let x15 of type ι → ο be given.
Let x16 of type ι → ο be given.
Let x17 of type ι → ι → ο be given.
Let x18 of type ι → ι → ο be given.
Let x19 of type ι be given.
Let x20 of type ι → ι → ι be given.
Let x21 of type ι → ι → ο be given.
Let x22 of type ι → ο be given.
Let x23 of type ι → ο be given.
Let x24 of type ι → ι be given.
Let x25 of type ι → ο be given.
Let x26 of type ι → ι → ι be given.
Let x27 of type ι be given.
Let x28 of type ι → ο be given.
Let x29 of type ι → ι be given.
Let x30 of type ι → ι be given.
Let x31 of type ι → ι → ι be given.
Let x32 of type ι → ι → ι be given.
Let x33 of type ι be given.
Let x34 of type ι → ο be given.
Let x35 of type ι → ο be given.
Let x36 of type ι be given.
Let x37 of type ι → ι → ι → ι → ο be given.
Let x38 of type ι → ι → ο be given.
Let x39 of type ι be given.
Let x40 of type ι be given.
Let x41 of type ι be given.
Let x42 of type ι be given.
Let x43 of type ι be given.
Let x44 of type ι → ι → ο be given.
Let x45 of type ι be given.
Let x46 of type ι → ι be given.
Let x47 of type ι → ι → ι be given.
Let x48 of type ι be given.
Let x49 of type ι be given.
Let x50 of type ι → ο be given.
Let x51 of type ι → ι → ο be given.
Let x52 of type ι → ι be given.
Let x53 of type ι be given.
Let x54 of type ι → ο be given.
Let x55 of type ι → ι → ο be given.
Let x56 of type ι → ι → ι be given.
Let x57 of type ι be given.
Let x58 of type ι → ο be given.
Let x59 of type ι be given.
Let x60 of type ι → ο be given.
Assume H5:
∀ x61 x62 . x60 x62 ⟶ (x62 = x61 ⟶ False) ⟶ x60 x61 ⟶ False.
Assume H6:
∀ x61 x62 . (x0 x62 ⟶ False) ⟶ x16 x62 ⟶ x1 x62 ⟶ x15 x61 ⟶ x3 x61 (x2 x62) (x2 x62) ⟶ x14 x61 (x2 x62) (x2 x62) ⟶ x4 x61 (x6 (x5 (x2 x62) (x2 x62))) ⟶ (x8 x62 (x7 (x2 x62) (x2 x62) x61 (x9 x61 x62)) (x7 (x2 x62) (x2 x62) x61 (x12 x61 x62)) (x7 (x2 x62) (x2 x62) x61 (x11 x61 x62)) (x7 (x2 x62) (x2 x62) x61 (x10 x61 x62)) ⟶ False) ⟶ (x8 x62 (x9 x61 x62) (x12 x61 x62) (x11 x61 x62) (x10 x61 x62) ⟶ False) ⟶ (x13 x61 x62 ⟶ False) ⟶ False.
Assume H7:
∀ x61 x62 . (x0 x62 ⟶ False) ⟶ x16 x62 ⟶ x1 x62 ⟶ x15 x61 ⟶ x3 x61 (x2 x62) (x2 x62) ⟶ x14 x61 (x2 x62) (x2 x62) ⟶ x4 x61 (x6 (x5 (x2 x62) (x2 x62))) ⟶ x8 x62 (x9 x61 x62) (x12 x61 x62) (x11 x61 x62) (x10 x61 x62) ⟶ x8 x62 (x7 (x2 x62) (x2 x62) x61 (x9 x61 x62)) (x7 (x2 x62) (x2 x62) x61 (x12 x61 x62)) (x7 (x2 x62) (x2 x62) x61 (x11 x61 x62)) (x7 (x2 x62) (x2 x62) x61 (x10 x61 x62)) ⟶ (x13 x61 x62 ⟶ False) ⟶ False.
Assume H8:
∀ x61 x62 . ... ⟶ ... ⟶ ... ⟶ ... ⟶ x3 x61 (x2 x62) (x2 x62) ⟶ x14 x61 (x2 x62) (x2 x62) ⟶ x4 x61 (x6 (x5 (x2 x62) (x2 x62))) ⟶ (x4 (x10 x61 x62) (x2 x62) ⟶ False) ⟶ (x13 x61 x62 ⟶ False) ⟶ False.