Claim L0: ...

...

Claim L1: ...

...

Claim L2: ...

...

Claim L3: ...

...

Claim L4: ...

...

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.

Assume H5: ∀ x47 x48 . x46 x48 ⟶ (x48 = x47 ⟶ False) ⟶ x46 x47 ⟶ False.

Assume H6: ∀ x47 x48 . x0 x47 x48 ⟶ x46 x48 ⟶ False.

Assume H7: ∀ x47 . x46 x47 ⟶ (x47 = x45 ⟶ False) ⟶ False.

Assume H8: ∀ x47 x48 . x0 x48 x47 ⟶ (x0 (x1 x48) (x1 x47) ⟶ False) ⟶ False.

Assume H9: ∀ x47 x48 . x44 x47 x48 ⟶ (x46 x48 ⟶ False) ⟶ (x0 x47 x48 ⟶ False) ⟶ False.

Assume H10: ∀ x47 x48 . x0 x48 x47 ⟶ (x44 x48 x47 ⟶ False) ⟶ False.

Assume H11: ∀ x47 x48 x49 . x43 x49 ⟶ x0 x48 x47 ⟶ x0 x47 x49 ⟶ (x0 x48 x49 ⟶ False) ⟶ False.

Assume H12: (x2 x3 ⟶ False) ⟶ False.

Assume H13: x46 x3 ⟶ False.

Assume H14: (x4 x5 ⟶ False) ⟶ False.

Assume H15: x46 x5 ⟶ False.

Assume H16: x6 x7 ⟶ False.

Assume H17: (x42 x7 ⟶ False) ⟶ False.

Assume H18: (x8 x7 ⟶ False) ⟶ False.

Assume H19: (x4 x41 ⟶ False) ⟶ False.

Assume H20: (x42 x9 ⟶ False) ⟶ False.

Assume H21: (x40 x9 ⟶ False) ⟶ False.

Assume H22: (x8 x9 ⟶ False) ⟶ False.

Assume H23: x46 x9 ⟶ False.

Assume H24: (x42 x10 ⟶ False) ⟶ False.

Assume H25: (x40 x10 ⟶ False) ⟶ False.

Assume H26: (x8 x10 ⟶ False) ⟶ False.

Assume H27: x46 x39 ⟶ False.

Assume H28: (x40 x11 ⟶ False) ⟶ False.

Assume H29: (x8 x11 ⟶ False) ⟶ False.

Assume H30: (x12 x13 ⟶ False) ⟶ False.

Assume H31: (x38 x13 ⟶ False) ⟶ False.

Assume H32: (x43 x13 ⟶ False) ⟶ False.

Assume H33: x46 x13 ⟶ False.

Assume H34: (x14 x15 ⟶ False) ⟶ False.

Assume H35: (x42 x15 ⟶ False) ⟶ False.

Assume H36: (x8 x15 ⟶ False) ⟶ False.

Assume H37: (x46 x37 ⟶ False) ⟶ False.

Assume H38: (x8 x16 ⟶ False) ⟶ False.

Assume H39: x46 x16 ⟶ False.

Assume H40: (x12 x17 ⟶ False) ⟶ False.

Assume H41: (x42 x36 ⟶ False) ⟶ False.

Assume H42: (x8 x36 ⟶ False) ⟶ False.

Assume H43: ∀ x47 . (x46 x47 ⟶ False) ⟶ x8 x47 ⟶ x46 (x35 x47) ⟶ False.

Assume H44: ∀ x47 x48 x49 x50 . (x8 (x18 (x19 x48 x47) (x19 x50 ...)) ⟶ False) ⟶ False.

...

■

Proofgold Proof