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

Apply unknownprop_f4200b1bfe9d1201eacbd1e98e7090f0808e8d20f165b84bde4d3035c1b2589a with 6b90c.. x0 x1, x2, x3, ∃ x4 . and (d7d78.. x0 x2 x4) (d7d78.. x1 x4 x3) leaving 11 subgoals.

The subproof is completed by applying H0.

Assume H1: 6b90c.. x0 x1 = c4def...

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

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

Apply unknownprop_edb5429996c91ec36192294fa1b04f517f52304f16c5634ffedaaf1a606af853 with x0, x1, x4, x5, x2 = x6 ⟶ x3 = x8 ⟶ ∃ x9 . and (d7d78.. x0 x2 x9) (d7d78.. x1 x9 x3) leaving 2 subgoals.

The subproof is completed by applying H3.

Assume H4: x0 = x4.

Assume H5: x1 = x5.

Assume H6: x2 = x6.

Assume H7: x3 = x8.

Let x9 of type ο be given.

Assume H8: ∀ x10 . and (d7d78.. x0 x2 x10) (d7d78.. x1 x10 x3) ⟶ x9.

Apply H8 with x7.

Apply andI with d7d78.. x0 x2 x7, d7d78.. x1 x7 x3 leaving 2 subgoals.

Apply H6 with λ x10 x11 . d7d78.. x0 x11 x7.

Apply H4 with λ x10 x11 . d7d78.. x11 x6 x7.

The subproof is completed by applying H1.

Apply H7 with λ x10 x11 . d7d78.. x1 x7 x11.

Apply H5 with λ x10 x11 . d7d78.. x11 x7 x8.

The subproof is completed by applying H2.

Assume H1: 6b90c.. x0 x1 = c9248...

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

Apply unknownprop_5af236d7c76b9f188cbf09c3f6d473027f96cf876457db19afeb6b2a20801c1c with x0, x1.

The subproof is completed by applying H1.

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

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

Apply unknownprop_0aa0d20c7475dff33a06f321231b328d61152f6c9f979f99ebc302846ee32935 with x0, x1, x4.

The subproof is completed by applying H2.

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

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

Apply unknownprop_47d331e63e660ea5a4e79a40706a07cfd71f39b2e79a55cbc3878e4671a0d1c7 with x0, x1, x4.

The subproof is completed by applying H2.

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: 6b90c.. x0 x1 = 3e00e.. x4 x5.

Apply FalseE with ... ⟶ ... ⟶ ∃ x9 . and ... ....

...

■

Proofgold Proof