Apply pred_ext_2 with cad8f.., 6b93f.. (4ae4a.. (4ae4a.. 4a7ef..)) leaving 2 subgoals.

Let x0 of type ι be given.

Apply H0 with λ x1 x2 . 6b93f.. (4ae4a.. (4ae4a.. 4a7ef..)) x1.

Let x1 of type ι be given.

Apply unknownprop_583e189228469f510dae093aa816b0d084f1acaf0341e7deab9d9a676d1b11ef with f482f.. x0 4a7ef.., f482f.. x0 (4ae4a.. 4a7ef..), x1, ∃ x2 . and (prim1 x2 (4ae4a.. (4ae4a.. 4a7ef..))) (∃ x3 . x1 = aae7a.. x2 x3) leaving 3 subgoals.

The subproof is completed by applying H1.

Assume H2: ∃ x2 . and (prim1 x2 (f482f.. x0 4a7ef..)) (x1 = aae7a.. 4a7ef.. x2).

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

The subproof is completed by applying H2.

Let x2 of type ι be given.

Assume H3: prim1 x2 (f482f.. x0 4a7ef..).

Assume H4: x1 = aae7a.. 4a7ef.. x2.

Let x3 of type ο be given.

Assume H5: ∀ x4 . and (prim1 x4 (4ae4a.. (4ae4a.. 4a7ef..))) (∃ x5 . x1 = aae7a.. x4 x5) ⟶ x3.

Apply H5 with 4a7ef...

Apply andI with prim1 4a7ef.. (4ae4a.. (4ae4a.. 4a7ef..)), ∃ x4 . x1 = aae7a.. 4a7ef.. x4 leaving 2 subgoals.

The subproof is completed by applying unknownprop_94c438c3f41134cd86e0be06a85b5e5b3aa8448f9221f51d2dfe9b1364042f49.

Let x4 of type ο be given.

Assume H6: ∀ x5 . x1 = aae7a.. 4a7ef.. x5 ⟶ x4.

Apply H6 with x2.

The subproof is completed by applying H4.

Assume H2: ∃ x2 . and (prim1 x2 (f482f.. x0 (4ae4a.. 4a7ef..))) (x1 = aae7a.. (4ae4a.. 4a7ef..) x2).

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

The subproof is completed by applying H2.

Let x2 of type ι be given.

Assume H4: x1 = aae7a.. (4ae4a.. 4a7ef..) x2.

Let x3 of type ο be given.

Assume H5: ∀ x4 . and (prim1 x4 (4ae4a.. (4ae4a.. 4a7ef..))) (∃ x5 . x1 = aae7a.. x4 x5) ⟶ x3.

Apply H5 with 4ae4a.. 4a7ef...

Apply andI with prim1 (4ae4a.. 4a7ef..) (4ae4a.. (4ae4a.. 4a7ef..)), ∃ x4 . x1 = aae7a.. (4ae4a.. 4a7ef..) x4 leaving 2 subgoals.

The subproof is completed by applying unknownprop_e256c3837ff221325e66d4c83283618d462d76cb96bca463e1abd4876bf63511.

Let x4 of type ο be given.

Assume H6: ∀ x5 . x1 = aae7a.. (4ae4a.. 4a7ef..) x5 ⟶ x4.

Apply H6 with x2.

The subproof is completed by applying H4.

Let x0 of type ι be given.

Apply unknownprop_5896ce98646deef8ec3dfd6486cb5e8ac723fe9e353ebdbde1d65018fd75b748 with x0.

Let x1 of type ι be given.

Assume H1: prim1 x1 x0.

Apply exandE_i with λ x2 . prim1 x2 (4ae4a.. (4ae4a.. ...)), ..., ... leaving 2 subgoals.

...

■

Proofgold Proof