Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: d7d78.. (1fa6d.. x0) x1 x2.

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

The subproof is completed by applying H0.

Assume H1: 1fa6d.. x0 = c4def...

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

Apply unknownprop_ef8c94d89928b9f62fee2a5f33da35b42cb09ce75d269714f659a763e2ceabd3 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: 1fa6d.. x0 = 6b90c.. x3 x4.

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

Apply unknownprop_80291db5c7bb264dbc82d5bd299a50466fd33dff5f553bcefc294dac43dc6508 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: 1fa6d.. x0 = c9248...

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

Apply unknownprop_624f0ef54e7cfbae2b8e5e62d9a7bcf99f188518d4958baceb268f4bc392e0b4 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: 1fa6d.. x0 = a6e19.. x3.

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

Apply unknownprop_8125183b2466cebd27df9418512f0d6ce0a70f4e488abb1536cd30c3faa9eafa 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: 1fa6d.. x0 = 2fe34.. x3.

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

Apply unknownprop_8cb3d88f411e1da99ec8e14728b2b5ae84352a193747718592c414163eeb0008 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: 1fa6d.. x0 = 3e00e.. x3 x4.

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

Apply unknownprop_e58a3603e39f9d98135354a057e6e0a8954b1aa29808bc27845c48ba595a7f9b 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: 1fa6d.. x0 = 3e00e.. x3 x4.

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

...

■

Proofgold Proof