Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: d7d78.. (2fe34.. x0) x1 x2.

Apply unknownprop_f4200b1bfe9d1201eacbd1e98e7090f0808e8d20f165b84bde4d3035c1b2589a with 2fe34.. x0, x1, x2, ∃ x3 . and (d7d78.. x0 x1 x3) (x2 = 6c5f4.. x3) leaving 11 subgoals.

The subproof is completed by applying H0.

Assume H1: 2fe34.. x0 = c4def...

Apply FalseE with x1 = x2 ⟶ ∃ x3 . and (d7d78.. x0 x1 x3) (x2 = 6c5f4.. x3).

Apply unknownprop_ee40677d5b822a93c478dc260b84724b662fdff27b19e5044867db6788e47b84 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: 2fe34.. x0 = 6b90c.. x3 x4.

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

Apply unknownprop_47d331e63e660ea5a4e79a40706a07cfd71f39b2e79a55cbc3878e4671a0d1c7 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: 2fe34.. x0 = c9248...

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

Apply unknownprop_89e1807665dc13acb478992379bb18c8ae07310598feb9724a2e1b2788427522 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: 2fe34.. x0 = a6e19.. x3.

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

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

Assume H3: x1 = x4.

Assume H4: x2 = 6c5f4.. x5.

Let x6 of type ο be given.

Assume H5: ∀ x7 . and (d7d78.. x0 x1 x7) (x2 = 6c5f4.. x7) ⟶ x6.

Apply H5 with x5.

Apply andI with d7d78.. x0 x1 x5, x2 = 6c5f4.. x5 leaving 2 subgoals.

Apply unknownprop_74f17c294ba427804301bb6754e40c47ff38c94bf925a96ad2f91d62c3719ba1 with x0, x3, λ x7 x8 . d7d78.. x8 x1 x5 leaving 2 subgoals.

The subproof is completed by applying H2.

Apply H3 with λ x7 x8 . d7d78.. x3 x8 x5.

The subproof is completed by applying H1.

The subproof is completed by applying H4.

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: 2fe34.. x0 = 3e00e.. x3 x4.

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

Apply unknownprop_2f36a5d84479af0c95a57f888d666236babb2eece004655ae6da48a516322088 with x0, x3, x4.

The subproof is completed by applying H3.

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.

...

■

Proofgold Proof