Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: d7d78.. (3a365.. x0) x1 x2.

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

The subproof is completed by applying H0.

Assume H1: 3a365.. x0 = c4def...

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

Apply unknownprop_ddb1c210f6c5076254ee217653e1ccbee3e92fbd92412f4de51e405856338853 with x0.

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

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

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.

Assume H1: d7d78.. x3 x5 x6.

Assume H2: d7d78.. x4 x6 x7.

Assume H3: 3a365.. x0 = 6b90c.. x3 x4.

Apply FalseE with x1 = x5 ⟶ x2 = x7 ⟶ ∃ x8 x9 . and (x1 = cfc98.. x8 x9) (d7d78.. x0 x9 x2).

Apply unknownprop_910e97be965e905e3df76d2620fcd238a9fcbe5e1671c0f8000ce6e5d29a875e with x3, x4, x0.

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

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

Assume H1: 3a365.. x0 = c9248...

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

Apply unknownprop_ee30ed1a8efd407b59c27b94f80f6fd7ae8c9d6ad4e49d17842925a37c8b681f with x0.

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

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

Let x3 of type ι be given.

Let x4 of type ι be given.

Let x5 of type ι be given.

Assume H1: d7d78.. x3 x4 x5.

Assume H2: 3a365.. x0 = a6e19.. x3.

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

Apply unknownprop_7b83de12fcc43ed9dd77c5bd18af0125fb6caf2fee9b0663650831117c46642f with x3, x0.

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

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

Let x3 of type ι be given.

Let x4 of type ι be given.

Let x5 of type ι be given.

Assume H1: d7d78.. x3 x4 x5.

Assume H2: 3a365.. x0 = 2fe34.. x3.

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

Apply unknownprop_b5c2a3f3ecbf8bc1f7ae2789852fa994d4025dc008e3b23f7a11dbe90d318452 with x3, x0.

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

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

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.

Assume H1: e05e6.. x4.

Assume H2: d7d78.. x3 (cfc98.. x5 x6) x7.

Assume H3: 3a365.. x0 = 3e00e.. x3 x4.

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

Apply unknownprop_7a30d7b2727f78067dd2d1e346284edb7e370623c1cd440ebde7b6371348111b with x3, x4, x0.

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

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

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.

Assume H1: e05e6.. x3.

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

Assume H3: 3a365.. x0 = 3e00e.. x3 x4.

Apply FalseE with ... ⟶ ... ⟶ ∃ x8 x9 . ....

...

■

Proofgold Proof