Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: d7d78.. (a6e19.. x0) x1 x2.

Apply unknownprop_f4200b1bfe9d1201eacbd1e98e7090f0808e8d20f165b84bde4d3035c1b2589a with a6e19.. x0, x1, x2, ∃ x3 . and (d7d78.. x0 x1 x3) (x2 = 0b8ef.. x3) leaving 11 subgoals.

The subproof is completed by applying H0.

Assume H1: a6e19.. x0 = c4def...

Apply FalseE with x1 = x2 ⟶ ∃ x3 . and (d7d78.. x0 x1 x3) (x2 = 0b8ef.. x3).

Apply unknownprop_1df3b42301db6867d78c685eafd354ebe7c61c16d5e29ce0846c97b25e8fb54c 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: a6e19.. x0 = 6b90c.. x3 x4.

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

Apply unknownprop_0aa0d20c7475dff33a06f321231b328d61152f6c9f979f99ebc302846ee32935 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: a6e19.. x0 = c9248...

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

Apply unknownprop_f451b8d81b6aaba93e0ee1e371b42dea54a5e7ff35bfed48f319c37f46604af7 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: a6e19.. x0 = a6e19.. x3.

Assume H3: x1 = x4.

Assume H4: x2 = 0b8ef.. x5.

Let x6 of type ο be given.

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

Apply H5 with x5.

Apply andI with d7d78.. x0 x1 x5, x2 = 0b8ef.. x5 leaving 2 subgoals.

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

Assume H1: d7d78.. x3 x4 x5.

Assume H2: a6e19.. x0 = 2fe34.. x3.

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

Apply unknownprop_019b9c316ef1c52e9bd99a526ec6870eac639342c47f009a33fa37b46b2b222c with x0, x3.

The subproof is completed by applying H2.

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

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

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

Assume H3: a6e19.. x0 = 3e00e.. ... ....

...

■

Proofgold Proof