Let x0 of type ι be given.

Apply set_ext with aae7a.. (4ae4a.. 4a7ef..) x0, 09364.. x0 leaving 2 subgoals.

Let x1 of type ι be given.

Assume H0: prim1 x1 (aae7a.. (4ae4a.. 4a7ef..) x0).

Apply unknownprop_c7550417d862f27710857dc7f3a47fd61afe15d66581922367eb5c5641bfab12 with 4ae4a.. 4a7ef.., x0, x1, prim1 x1 (09364.. x0) leaving 3 subgoals.

The subproof is completed by applying H0.

Assume H1: ∃ x2 . and (prim1 x2 (4ae4a.. 4a7ef..)) (x1 = f6917.. x2).

Apply exandE_i with λ x2 . prim1 x2 (4ae4a.. 4a7ef..), λ x2 . x1 = f6917.. x2, prim1 x1 (09364.. x0) leaving 2 subgoals.

The subproof is completed by applying H1.

Let x2 of type ι be given.

Assume H2: prim1 x2 (4ae4a.. 4a7ef..).

Assume H3: x1 = f6917.. x2.

Apply H3 with λ x3 x4 . prim1 x4 (09364.. x0).

Claim L4: x2 = 4a7ef..

Apply unknownprop_30833a9978e304b25ffd59c347245315985872140acc9e441a97543a28184d79 with 4a7ef.., x2.

Apply unknownprop_745f0ddae55929306ce167ef9bae0ede767961c0319e8b14305a55d5b24d73e4 with x2.

The subproof is completed by applying H2.

Apply L4 with λ x3 x4 . prim1 (f6917.. x4) (09364.. x0).

Apply unknownprop_b28cc188f8a4b4b04f2650d497cfb7b037b6dc06850ad64a10472fb99bf8c330 with λ x3 x4 . prim1 x4 (09364.. x0).

The subproof is completed by applying unknownprop_f2280590a4843dd3047de5e5151d043be723c7f73a981e4edcbfbfe0904566e7 with x0.

Assume H1: ∃ x2 . and (prim1 x2 x0) (x1 = 09364.. x2).

Apply exandE_i with λ x2 . prim1 x2 x0, λ x2 . x1 = 09364.. x2, prim1 x1 (09364.. x0) leaving 2 subgoals.

The subproof is completed by applying H1.

Let x2 of type ι be given.

Assume H2: prim1 x2 x0.

Assume H3: x1 = 09364.. x2.

Apply H3 with λ x3 x4 . prim1 x4 (09364.. x0).

Apply unknownprop_83de80e22aba688e4d8cf3ccc9ec372406ae5110cef0bf0846317bfd1d974b00 with x0, x2.

The subproof is completed by applying H2.

Let x1 of type ι be given.

Assume H0: prim1 x1 (09364.. x0).

Apply unknownprop_b16c51a027be568304bbf4d10214f2f7bab4a7ef1f3929990ec85447bbbf7c12 with x0, x1, prim1 x1 (aae7a.. (4ae4a.. 4a7ef..) x0) leaving 3 subgoals.

The subproof is completed by applying H0.

Assume H1: x1 = 4a7ef...

Apply H1 with λ x2 x3 . prim1 x3 (aae7a.. (4ae4a.. 4a7ef..) x0).

Apply unknownprop_b28cc188f8a4b4b04f2650d497cfb7b037b6dc06850ad64a10472fb99bf8c330 with λ x2 x3 . prim1 x2 (aae7a.. (4ae4a.. 4a7ef..) x0).

Apply unknownprop_8f6cc176a3f8bf2c7f1eddd738c1f22ef319b214b1baddc301c61e34c7bade15 with 4ae4a.. 4a7ef.., x0, 4a7ef...

The subproof is completed by applying unknownprop_375af585d676cd889234cd20860ce45033e1ffceb375ac6277c1b1a2e16f15bd.

Assume H1: ∃ x2 . and (prim1 x2 x0) (x1 = 09364.. x2).

Apply exandE_i with λ x2 . prim1 x2 x0, λ x2 . x1 = 09364.. x2, prim1 x1 (aae7a.. (4ae4a.. 4a7ef..) x0) leaving 2 subgoals.

The subproof is completed by applying H1.

Let x2 of type ι be given.

Assume H2: prim1 x2 x0.

Assume H3: x1 = 09364.. x2.

Apply H3 with λ x3 x4 . prim1 x4 (aae7a.. (4ae4a.. 4a7ef..) x0).

Apply unknownprop_21bfd05a2dded69408d4a77ad07f3965317c49d7fa73834904d6def11389f597 with 4ae4a.. 4a7ef.., x0, x2.

The subproof is completed by applying H2.

■

Proofgold Proof