Let x0 of type ι be given.

Apply unknownprop_1b764290fde7c6be5dad24a6a257b6d0c773613bb687261020b529743ed07853 with setexp 2 x0, Power x0.

Apply unknownprop_4b95783dcb3eee1943e1de5542f675166ef402c8fbdda80bdf0920b55d3fc6de with setexp 2 x0, Power x0, λ x1 . Sep x0 (λ x2 . ap x1 x2 = 1).

Apply unknownprop_aa42ade5598d8612d2029318c4ed81646c550ecc6cdd9ab953ce4bf73f3dd562 with setexp 2 x0, Power x0, λ x1 . Sep x0 (λ x2 . ap x1 x2 = 1) leaving 2 subgoals.

Apply unknownprop_57c8600e4bc6abecef2ae17962906fa2de1fc16f5d46ed100ff99cd5b67f5b1b with setexp 2 x0, Power x0, λ x1 . Sep x0 (λ x2 . ap x1 x2 = 1) leaving 2 subgoals.

Let x1 of type ι be given.

Assume H0: In x1 (setexp 2 x0).

The subproof is completed by applying unknownprop_c9c2e69f88d46844ae70fe42f534424177b684dc2c45e594a43c8051db90fe17 with x0, λ x2 . ap x1 x2 = 1.

Let x1 of type ι be given.

Assume H0: In x1 (setexp 2 x0).

Let x2 of type ι be given.

Assume H1: In x2 (setexp 2 x0).

Assume H2: Sep x0 (λ x3 . ap x1 x3 = 1) = Sep x0 (λ x3 . ap x2 x3 = 1).

Apply unknownprop_23208921203993e7c79234f69a10e3d42c3011a560c83fb48a9d1a8f3b50675c with x0, 2, 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.

Claim L4: In (ap x1 x3) 2

Apply unknownprop_0850c5650a2b96b400e4741e4dbd234b5337d397bb9bfabc1463651d86151ddb with x0, 2, x1, x3 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H3.

Claim L5: In (ap x2 x3) 2

Apply unknownprop_0850c5650a2b96b400e4741e4dbd234b5337d397bb9bfabc1463651d86151ddb with x0, 2, x2, x3 leaving 2 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H3.

Apply unknownprop_ba6d0de3ea1c2beeca9d6a57f630aeac271753c66312f1f2e9496df2b38ad2c6 with ap x2 x3, λ x4 . ap x2 x3 = x4 ⟶ ap x1 x3 = x4 leaving 4 subgoals.

The subproof is completed by applying L5.

Assume H6: ap x2 x3 = 0.

Apply unknownprop_ba6d0de3ea1c2beeca9d6a57f630aeac271753c66312f1f2e9496df2b38ad2c6 with ap x1 x3, λ x4 . ap x1 x3 = x4 ⟶ x4 = 0 leaving 4 subgoals.

The subproof is completed by applying L4.

Assume H7: ap x1 x3 = 0.

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

Assume H8: x4 0 0.

The subproof is completed by applying H8.

Assume H7: ap x1 x3 = 1.

Claim L8: In x3 (Sep x0 (λ x4 . ap x2 x4 = 1))

Apply H2 with λ x4 x5 . In x3 x4.

Apply unknownprop_646b3add51cf8f8e84959b456822a93c7e59b2f394a14897b6752b9d28c1a75d with x0, λ x4 . ap x1 x4 = 1, x3 leaving 2 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H7.

Apply unknownprop_ba186f550679124419b8222be99b3e20dd42619ae850577f6f9edb2a83aac5a7 with x0, λ x4 . ap x2 x4 = 1, x3, λ x4 x5 . x4 = 0 leaving 2 subgoals.

The subproof is completed by applying L8.

The subproof is completed by applying H6.

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

Assume H7: x4 (ap x1 x3) (ap x1 x3).

The subproof is completed by applying H7.

Assume H6: ap x2 x3 = 1.

Claim L7: In x3 (Sep x0 (λ x4 . ap x1 x4 = 1))

Apply H2 with λ x4 x5 . In x3 x5.

Apply unknownprop_646b3add51cf8f8e84959b456822a93c7e59b2f394a14897b6752b9d28c1a75d with x0, λ x4 . ap x2 x4 = 1, x3 leaving 2 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H6.

Apply unknownprop_ba186f550679124419b8222be99b3e20dd42619ae850577f6f9edb2a83aac5a7 with x0, λ x4 . ap x1 x4 = 1, x3.

The subproof is completed by applying L7.

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

Assume H6: x4 (ap x2 x3) (ap x2 x3).

The subproof is completed by applying H6.

Let x1 of type ι be given.

Assume H0: In x1 (Power x0).

...

■

Proofgold Proof