Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Claim L1: ∃ x4 . and (prim1 x4 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (∃ x5 . and (prim1 x5 (If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 x2))) (x3 = aae7a.. x4 x5))

Apply unknownprop_d4dc73f3cbfe4c22363272ac418d035b8e77c49433b0870b96bee8fa9c46bfcf with 4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)), λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 x2), x3.

The subproof is completed by applying H0.

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

The subproof is completed by applying L1.

Let x4 of type ι be given.

Assume H3: ∃ x5 . and (prim1 x5 (If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 x2))) (x3 = aae7a.. x4 x5).

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

The subproof is completed by applying H3.

Let x5 of type ι be given.

Assume H4: prim1 x5 (If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 x2)).

Assume H5: x3 = aae7a.. x4 x5.

Let x6 of type ο be given.

Assume H6: ∀ x7 . and (prim1 x7 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (∃ x8 . x3 = aae7a.. x7 x8) ⟶ x6.

Apply H6 with x4.

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

The subproof is completed by applying H2.

Let x7 of type ο be given.

Assume H7: ∀ x8 . x3 = aae7a.. x4 x8 ⟶ x7.

Apply H7 with x5.

The subproof is completed by applying H5.

■

Proofgold Proof