Let x0 of type ι be given.

Let x1 of type ι → ι be given.

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

Let x3 of type ι be given.

Assume H0: prim1 x3 (38062.. x0 x1 x2).

Apply unknownprop_d516324acb9cecc54a3dc4c9e001108ae079249b9f74b554177899d61add34ac with x0, x1, x2, x3, ∃ x4 x5 . x3 = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x6 . If_i (x6 = 4a7ef..) x4 x5) leaving 2 subgoals.

The subproof is completed by applying H0.

Let x4 of type ι be given.

Assume H1: (λ x5 . and (prim1 x5 x0) (∃ x6 . and (prim1 x6 (x1 x5)) (and (x3 = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x7 . If_i (x7 = 4a7ef..) x5 x6)) (x2 x5 x6)))) x4.

Apply H1 with ∃ x5 x6 . x3 = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x7 . If_i (x7 = 4a7ef..) x5 x6).

Assume H2: prim1 x4 x0.

Assume H3: ∃ x5 . and (prim1 x5 (x1 x4)) (and (x3 = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x6 . If_i (x6 = 4a7ef..) x4 x5)) (x2 x4 x5)).

Apply H3 with ∃ x5 x6 . x3 = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x7 . If_i (x7 = 4a7ef..) x5 x6).

Let x5 of type ι be given.

Assume H4: (λ x6 . and (prim1 x6 (x1 x4)) (and (x3 = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x7 . If_i (x7 = 4a7ef..) x4 x6)) (x2 x4 x6))) x5.

Apply H4 with ∃ x6 x7 . x3 = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x8 . If_i (x8 = 4a7ef..) x6 x7).

Assume H5: prim1 x5 (x1 x4).

Assume H6: and (x3 = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x6 . If_i (x6 = 4a7ef..) x4 x5)) (x2 x4 x5).

Apply H6 with ∃ x6 x7 . x3 = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x8 . If_i (x8 = 4a7ef..) x6 x7).

Assume H7: x3 = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x6 . If_i (x6 = 4a7ef..) x4 x5).

Assume H8: x2 x4 x5.

Let x6 of type ο be given.

Assume H9: ∀ x7 . (∃ x8 . x3 = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x9 . If_i (x9 = 4a7ef..) x7 x8)) ⟶ x6.

Apply H9 with x4.

Let x7 of type ο be given.

Assume H10: ∀ x8 . x3 = 0fc90.. (4ae4a.. (4ae4a.. 4a7ef..)) (λ x9 . If_i (x9 = 4a7ef..) x4 x8) ⟶ x7.

Apply H10 with x5.

The subproof is completed by applying H7.

■

Proofgold Proof