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 . x1 x47 x48 ⟶ (x46 x48 ⟶ False) ⟶ (x0 x47 x48 ⟶ False) ⟶ False.

Assume H9: ∀ x47 x48 x49 x50 . x44 x48 x50 = x44 x47 x49 ⟶ (x50 = x49 ⟶ False) ⟶ False.

Assume H10: ∀ x47 x48 x49 x50 . x44 x50 x48 = x44 x49 x47 ⟶ (x50 = x49 ⟶ False) ⟶ False.

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

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

Assume H13: x46 x3 ⟶ False.

Assume H14: x4 x5 ⟶ False.

Assume H15: (x43 x5 ⟶ False) ⟶ False.

Assume H16: (x6 x5 ⟶ False) ⟶ False.

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

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

Assume H19: (x6 x42 ⟶ False) ⟶ False.

Assume H20: x46 x42 ⟶ False.

Assume H21: (x43 x41 ⟶ False) ⟶ False.

Assume H22: (x7 x41 ⟶ False) ⟶ False.

Assume H23: (x6 x41 ⟶ False) ⟶ False.

Assume H24: x8 x9 ⟶ False.

Assume H25: x46 x40 ⟶ False.

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

Assume H27: (x6 x10 ⟶ False) ⟶ False.

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

Assume H29: (x43 x12 ⟶ False) ⟶ False.

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

Assume H31: x46 x39 ⟶ False.

Assume H32: (x4 x39 ⟶ False) ⟶ False.

Assume H33: (x43 x39 ⟶ False) ⟶ False.

Assume H34: (x6 x39 ⟶ False) ⟶ False.

Assume H35: (x8 x38 ⟶ False) ⟶ False.

Assume H36: x46 x38 ⟶ False.

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

Assume H38: (x6 x13 ⟶ False) ⟶ False.

Assume H39: x46 x13 ⟶ False.

Assume H40: (x43 x14 ⟶ False) ⟶ False.

Assume H41: (x6 x14 ⟶ False) ⟶ False.

Assume H42: (x15 x16 ⟶ False) ⟶ False.

Assume H43: (x43 x16 ⟶ False) ⟶ False.

Assume H44: (x6 x16 ⟶ False) ⟶ False.

Assume H45: ∀ x47 . (x46 x47 ⟶ False) ⟶ x6 x47 ⟶ x46 (x36 x47) ⟶ False.

Assume H46: ∀ x47 x48 . ... ⟶ ... ⟶ ... ⟶ (... ⟶ False) ⟶ False.

...

■

Proofgold Proof