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.. (f9341.. x0 x1) x2 x3.

Apply unknownprop_f4200b1bfe9d1201eacbd1e98e7090f0808e8d20f165b84bde4d3035c1b2589a with f9341.. x0 x1, x2, x3, ∃ x4 x5 . and (and (d7d78.. x0 x2 x4) (d7d78.. x1 x2 x5)) (x3 = cfc98.. x4 x5) leaving 11 subgoals.

The subproof is completed by applying H0.

Assume H1: f9341.. x0 x1 = c4def...

Apply FalseE with x2 = x3 ⟶ ∃ x4 x5 . and (and (d7d78.. x0 x2 x4) (d7d78.. x1 x2 x5)) (x3 = cfc98.. x4 x5).

Apply unknownprop_f0d13e3fa17fec253e15aec42ff29f78d0f34dc71d8440d7fbd29d362401dd86 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: f9341.. x0 x1 = 6b90c.. x4 x5.

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

Apply unknownprop_c2589a424613d398f5170ff6a9af4021a319753aeb6bc765bd532fd384314bdd 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: f9341.. x0 x1 = c9248...

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

Apply unknownprop_67c2c56d186d56a804c2dcef7756a8fc60ff20cadf66c8f302d4b16b1cd25d21 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: f9341.. x0 x1 = a6e19.. x4.

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

Apply unknownprop_347361a4866f321dcbd1b268e37b5f82a9cdfe5f028393dc0e425c03fd837f67 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.

Assume H2: f9341.. x0 x1 = 2fe34.. x4.

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

Apply unknownprop_746a6e3f17cb77c2f78d96396456f419d118c216d18a5ae70c1934532bf48383 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.

Let x7 of type ι be given.

Let x8 of type ι be given.

Assume H1: e05e6.. x5.

Assume H2: d7d78.. x4 (cfc98.. x6 x7) x8.

Assume H3: f9341.. x0 x1 = 3e00e.. x4 x5.

Apply FalseE with ... ⟶ ... ⟶ ∃ x9 x10 . and (and (d7d78.. x0 x2 x9) ...) ....

...

■

Proofgold Proof