Let x0 of type ι be given.

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: (λ x3 . Sep x0 (λ x4 . ap x3 x4 = 1)) x1 = (λ x3 . Sep x0 (λ x4 . ap x3 x4 = 1)) x2.

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: ...

...

Claim L5: ...

...

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

The subproof is completed by applying L4.

Assume H6: ap x1 x3 = 0.

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

The subproof is completed by applying L5.

Assume H7: ap x2 x3 = 0.

set y4 to be ap x1 x3

set y5 to be ap x3 y4

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

Let x6 of type ι → ο be given.

Assume H8: x6 (ap y4 y5).

Apply H6 with λ x7 . x6.

set y7 to be λ x7 . x6

Apply H7 with λ x8 x9 . y7 x9 x8.

The subproof is completed by applying H8.

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

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

Assume H9: x6 y5 y5.

The subproof is completed by applying H9.

Assume H7: ap x2 x3 = 1.

Apply FalseE with ap x1 x3 = ap x2 x3.

Claim L8: In x3 ((λ x4 . Sep x0 (λ x5 . ap x4 x5 = 1)) x1) ⟶ False

Assume H8: In x3 (Sep x0 (λ x4 . ap x1 x4 = 1)).

Apply notE with 0 = 1 leaving 2 subgoals.

The subproof is completed by applying unknownprop_e1454ae89380849e3cb6b4743b200bdcbe47a12d25b42c4b1d68a2f07dac0ac1.

Apply H6 with λ x4 x5 . x4 = 1.

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

The subproof is completed by applying H8.

Apply L8.

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 H7.

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

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

The subproof is completed by applying H7.

Assume H6: ap x1 x3 = 1.

Apply unknownprop_ba6d0de3ea1c2beeca9d6a57f630aeac271753c66312f1f2e9496df2b38ad2c6 with ap x2 ..., ... leaving 4 subgoals.

...

■

Proofgold Proof