Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H0: d7d78.. (3e00e.. x0 x1) x2 x3.

Apply unknownprop_f4200b1bfe9d1201eacbd1e98e7090f0808e8d20f165b84bde4d3035c1b2589a with 3e00e.. x0 x1, x2, x3, or (∃ x4 x5 . and (x2 = cfc98.. (0b8ef.. x4) x5) (d7d78.. x0 (cfc98.. x4 x5) x3)) (∃ x4 x5 . and (x2 = cfc98.. (6c5f4.. x4) x5) (d7d78.. x1 (cfc98.. x4 x5) x3)) leaving 11 subgoals.

The subproof is completed by applying H0.

Assume H1: 3e00e.. x0 x1 = c4def...

Apply FalseE with x2 = x3 ⟶ or (∃ x4 x5 . and (x2 = cfc98.. (0b8ef.. x4) x5) (d7d78.. x0 (cfc98.. x4 x5) x3)) (∃ x4 x5 . and (x2 = cfc98.. (6c5f4.. x4) x5) (d7d78.. x1 (cfc98.. x4 x5) x3)).

Apply unknownprop_542d83ffac2c2ef082f7823f9f5feddbe3dddeda752b3a3ce5c0b8f5e5bd0dd3 with x0, x1.

Let x4 of type ι → ι → ο be given.

The subproof is completed by applying H1 with λ x5 x6 . x4 x6 x5.

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.

Assume H1: d7d78.. x4 x6 x7.

Assume H2: d7d78.. x5 x7 x8.

Assume H3: 3e00e.. x0 x1 = 6b90c.. x4 x5.

Apply FalseE with x2 = x6 ⟶ x3 = x8 ⟶ or (∃ x9 x10 . and (x2 = cfc98.. (0b8ef.. x9) x10) (d7d78.. x0 (cfc98.. x9 x10) x3)) (∃ x9 x10 . and (x2 = cfc98.. (6c5f4.. x9) x10) (d7d78.. x1 (cfc98.. x9 x10) x3)).

Apply unknownprop_11d5d6371e6b2745f54b892cf4c3d2b2149e50cfcf0d94399ec8a6b529e85501 with x4, x5, x0, x1.

Let x9 of type ι → ι → ο be given.

The subproof is completed by applying H3 with λ x10 x11 . x9 x11 x10.

Assume H1: 3e00e.. x0 x1 = c9248...

Apply FalseE with x3 = 236c6.. ⟶ or (∃ x4 x5 . and (x2 = cfc98.. (0b8ef.. x4) x5) (d7d78.. x0 (cfc98.. x4 x5) x3)) (∃ x4 x5 . and (x2 = cfc98.. (6c5f4.. x4) x5) (d7d78.. x1 (cfc98.. x4 x5) x3)).

Apply unknownprop_507309b6c879edba011aec54390184479ff16bf6d908b329864df6b6f9c5b92e with x0, x1.

Let x4 of type ι → ι → ο be given.

The subproof is completed by applying H1 with λ x5 x6 . x4 x6 x5.

Let x4 of type ι be given.

Let x5 of type ι be given.

Let x6 of type ι be given.

Assume H1: d7d78.. x4 x5 x6.

Assume H2: 3e00e.. x0 x1 = a6e19.. x4.

Apply FalseE with x2 = x5 ⟶ x3 = 0b8ef.. x6 ⟶ or (∃ x7 x8 . and (x2 = cfc98.. (0b8ef.. x7) x8) (d7d78.. x0 (cfc98.. x7 x8) x3)) (∃ x7 x8 . and (x2 = cfc98.. (6c5f4.. x7) x8) (d7d78.. x1 (cfc98.. x7 x8) x3)).

Apply unknownprop_7b8bf45e42524757958b599bfbf2d3d7d26e0458e1dc0a2d37f57e00c77a41a4 with x4, x0, x1.

Let x7 of type ι → ι → ο be given.

The subproof is completed by applying H2 with λ x8 x9 . x7 x9 x8.

Let x4 of type ι be given.

Let x5 of type ι be given.

Let x6 of type ι be given.

Assume H1: d7d78.. x4 x5 x6.

...

■

Proofgold Proof