Let x0 of type ι be given.

Let x1 of type ι be given.

Apply unknownprop_f4200b1bfe9d1201eacbd1e98e7090f0808e8d20f165b84bde4d3035c1b2589a with c9248.., x0, x1, x1 = 236c6.. leaving 11 subgoals.

The subproof is completed by applying H0.

Assume H1: c9248.. = c4def...

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

Apply unknownprop_82ec982050a62cae4481cf9ebd68e2d43efe2c0ff63af3c8637362b2fcfa39ef.

Let x2 of type ι → ι → ο be given.

The subproof is completed by applying H1 with λ x3 x4 . x2 x4 x3.

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: c9248.. = 6b90c.. x2 x3.

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

Apply unknownprop_5af236d7c76b9f188cbf09c3f6d473027f96cf876457db19afeb6b2a20801c1c with x2, x3.

Let x7 of type ι → ι → ο be given.

The subproof is completed by applying H3 with λ x8 x9 . x7 x9 x8.

Assume H1: c9248.. = c9248...

Assume H2: x1 = 236c6...

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: c9248.. = a6e19.. x2.

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

Apply unknownprop_f451b8d81b6aaba93e0ee1e371b42dea54a5e7ff35bfed48f319c37f46604af7 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: c9248.. = 2fe34.. x2.

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

Apply unknownprop_89e1807665dc13acb478992379bb18c8ae07310598feb9724a2e1b2788427522 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: c9248.. = 3e00e.. x2 x3.

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

Apply unknownprop_507309b6c879edba011aec54390184479ff16bf6d908b329864df6b6f9c5b92e 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: c9248.. = 3e00e.. x2 x3.

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

Apply unknownprop_507309b6c879edba011aec54390184479ff16bf6d908b329864df6b6f9c5b92e 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: c9248.. = f9341.. x2 x3.

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

Apply unknownprop_67c2c56d186d56a804c2dcef7756a8fc60ff20cadf66c8f302d4b16b1cd25d21 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: c9248.. = 1fa6d.. x2.

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

Apply unknownprop_624f0ef54e7cfbae2b8e5e62d9a7bcf99f188518d4958baceb268f4bc392e0b4 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: c9248.. = 3a365.. x2.

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

...

■

Proofgold Proof