Let x0 of type ι be given.

Let x1 of type ι be given.

Apply unknownprop_f4200b1bfe9d1201eacbd1e98e7090f0808e8d20f165b84bde4d3035c1b2589a with c4def.., x0, x1, x0 = x1 leaving 11 subgoals.

The subproof is completed by applying H0.

Assume H1: c4def.. = c4def...

Assume H2: x0 = x1.

The subproof is completed by applying H2.

Let x2 of type ι be given.

Let x3 of type ι be given.

Let x4 of type ι be given.

Let x5 of type ι be given.

Let x6 of type ι be given.

Assume H1: d7d78.. x2 x4 x5.

Assume H2: d7d78.. x3 x5 x6.

Assume H3: c4def.. = 6b90c.. x2 x3.

Apply FalseE with x0 = x4 ⟶ x1 = x6 ⟶ x0 = x1.

Apply unknownprop_7cf6ac9a00e44baaefc01c770659af5ae1a9bfc94e963f6bf246a920439f528b with x2, x3.

The subproof is completed by applying H3.

Assume H1: c4def.. = c9248...

Apply FalseE with x1 = 236c6.. ⟶ x0 = x1.

Apply unknownprop_82ec982050a62cae4481cf9ebd68e2d43efe2c0ff63af3c8637362b2fcfa39ef.

The subproof is completed by applying H1.

Let x2 of type ι be given.

Let x3 of type ι be given.

Let x4 of type ι be given.

Assume H1: d7d78.. x2 x3 x4.

Assume H2: c4def.. = a6e19.. x2.

Apply FalseE with x0 = x3 ⟶ x1 = 0b8ef.. x4 ⟶ x0 = x1.

Apply unknownprop_1df3b42301db6867d78c685eafd354ebe7c61c16d5e29ce0846c97b25e8fb54c with x2.

The subproof is completed by applying H2.

Let x2 of type ι be given.

Let x3 of type ι be given.

Let x4 of type ι be given.

Assume H1: d7d78.. x2 x3 x4.

Assume H2: c4def.. = 2fe34.. x2.

Apply FalseE with x0 = x3 ⟶ x1 = 6c5f4.. x4 ⟶ x0 = x1.

Apply unknownprop_ee40677d5b822a93c478dc260b84724b662fdff27b19e5044867db6788e47b84 with x2.

The subproof is completed by applying H2.

Let x2 of type ι be given.

Let x3 of type ι be given.

Let x4 of type ι be given.

Let x5 of type ι be given.

Let x6 of type ι be given.

Assume H1: e05e6.. x3.

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

Assume H3: c4def.. = 3e00e.. x2 x3.

Apply FalseE with x0 = cfc98.. (0b8ef.. x4) x5 ⟶ x1 = x6 ⟶ x0 = x1.

Apply unknownprop_542d83ffac2c2ef082f7823f9f5feddbe3dddeda752b3a3ce5c0b8f5e5bd0dd3 with x2, x3.

The subproof is completed by applying H3.

Let x2 of type ι be given.

Let x3 of type ι be given.

Let x4 of type ι be given.

Let x5 of type ι be given.

Let x6 of type ι be given.

Assume H1: e05e6.. x2.

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

Assume H3: c4def.. = 3e00e.. x2 x3.

Apply FalseE with x0 = cfc98.. (6c5f4.. x4) x5 ⟶ x1 = x6 ⟶ x0 = x1.

Apply unknownprop_542d83ffac2c2ef082f7823f9f5feddbe3dddeda752b3a3ce5c0b8f5e5bd0dd3 with x2, x3.

The subproof is completed by applying H3.

Let x2 of type ι be given.

Let x3 of type ι be given.

Let x4 of type ι be given.

Let x5 of type ι be given.

Let x6 of type ι be given.

Assume H1: d7d78.. x2 x4 x5.

Assume H2: d7d78.. x3 x4 x6.

Assume H3: c4def.. = f9341.. x2 x3.

Apply FalseE with x0 = x4 ⟶ x1 = cfc98.. x5 x6 ⟶ x0 = x1.

Apply unknownprop_f0d13e3fa17fec253e15aec42ff29f78d0f34dc71d8440d7fbd29d362401dd86 with x2, x3.

The subproof is completed by applying H3.

Let x2 of type ι be given.

Let x3 of type ι be given.

Let x4 of type ι be given.

Let x5 of type ι be given.

Assume H1: d7d78.. x2 x3 x5.

Assume H2: c4def.. = 1fa6d.. x2.

Apply FalseE with x0 = cfc98.. x3 x4 ⟶ x1 = x5 ⟶ x0 = x1.

Apply unknownprop_ef8c94d89928b9f62fee2a5f33da35b42cb09ce75d269714f659a763e2ceabd3 with x2.

The subproof is completed by applying H2.

Let x2 of type ι be given.

Let x3 of type ι be given.

Let x4 of type ι be given.

Let x5 of type ι be given.

Assume H1: d7d78.. x2 x4 x5.

Assume H2: c4def.. = 3a365.. x2.

Apply FalseE with x0 = cfc98.. x3 x4 ⟶ x1 = x5 ⟶ x0 = x1.

Apply unknownprop_ddb1c210f6c5076254ee217653e1ccbee3e92fbd92412f4de51e405856338853 with x2.

The subproof is completed by applying H2.

■

Proofgold Proof