Let x0 of type ι be given.

Apply unknownprop_4b95783dcb3eee1943e1de5542f675166ef402c8fbdda80bdf0920b55d3fc6de with setexp 1 x0, 1, λ x1 . 0.

Apply unknownprop_aa42ade5598d8612d2029318c4ed81646c550ecc6cdd9ab953ce4bf73f3dd562 with setexp 1 x0, 1, λ x1 . 0 leaving 2 subgoals.

Apply unknownprop_57c8600e4bc6abecef2ae17962906fa2de1fc16f5d46ed100ff99cd5b67f5b1b with setexp 1 x0, 1, λ x1 . 0 leaving 2 subgoals.

Let x1 of type ι be given.

Assume H0: In x1 (setexp 1 x0).

The subproof is completed by applying unknownprop_b28daf094ddd549776d741eec1dac894d28f0f162bae7bdbdbfb7366b31cdef0.

Let x1 of type ι be given.

Assume H0: In x1 (setexp 1 x0).

Let x2 of type ι be given.

Assume H1: In x2 (setexp 1 x0).

Assume H2: (λ x3 . 0) x1 = (λ x3 . 0) x2.

Apply unknownprop_23208921203993e7c79234f69a10e3d42c3011a560c83fb48a9d1a8f3b50675c with x0, 1, x1, x2 leaving 3 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

Let x3 of type ι be given.

Assume H3: In x3 x0.

set y4 to be ap x1 x3

set y5 to be ap x3 y4

Claim L4: ∀ x6 : ι → ο . x6 y5 ⟶ x6 y4

Let x6 of type ι → ο be given.

Assume H4: x6 (ap y4 y5).

Apply unknownprop_7f6501f9f8c19f5c2cddf4168679e2ff20a237333cd0d098eed3a3984bc044c0 with ap x3 y5, λ x7 . x7 = 0, λ x7 . x6 leaving 3 subgoals.

Apply unknownprop_0850c5650a2b96b400e4741e4dbd234b5337d397bb9bfabc1463651d86151ddb with x2, 1, x3, y5 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H3.

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

Assume H5: x7 0 0.

The subproof is completed by applying H5.

Apply unknownprop_7f6501f9f8c19f5c2cddf4168679e2ff20a237333cd0d098eed3a3984bc044c0 with ap y4 y5, λ x7 . 0 = x7, λ x7 . x6 leaving 3 subgoals.

Apply unknownprop_0850c5650a2b96b400e4741e4dbd234b5337d397bb9bfabc1463651d86151ddb with x2, 1, y4, y5 leaving 2 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H3.

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

Assume H5: x7 0 0.

The subproof is completed by applying H5.

The subproof is completed by applying H4.

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

Apply L4 with λ x7 . x6 x7 y5 ⟶ x6 y5 x7.

Assume H5: x6 y5 y5.

The subproof is completed by applying H5.

Let x1 of type ι be given.

Assume H0: In x1 1.

Let x2 of type ο be given.

Assume H1: ∀ x3 . and (In x3 (setexp 1 x0)) ((λ x4 . 0) x3 = x1) ⟶ x2.

Apply H1 with lam x0 (λ x3 . 0).

Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with In (lam x0 (λ x3 . 0)) (setexp 1 x0), (λ x3 . 0) (lam x0 (λ x3 . 0)) = x1 leaving 2 subgoals.

Apply unknownprop_204aaff43997dfdee1bf2ffda080faf1153e7eb6d169528444a836fe2ecc543c with x0, 1, λ x3 . 0.

Let x3 of type ι be given.

Assume H2: In x3 x0.

The subproof is completed by applying unknownprop_b28daf094ddd549776d741eec1dac894d28f0f162bae7bdbdbfb7366b31cdef0.

Apply unknownprop_7f6501f9f8c19f5c2cddf4168679e2ff20a237333cd0d098eed3a3984bc044c0 with x1, λ x3 . 0 = x3 leaving 2 subgoals.

The subproof is completed by applying H0.

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

Assume H2: x3 0 0.

The subproof is completed by applying H2.

■

Proofgold Proof