Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H0: In x2 x1.

Apply unknownprop_4b95783dcb3eee1943e1de5542f675166ef402c8fbdda80bdf0920b55d3fc6de with setexp x0 x1, setprod x0 (setexp x0 (setminus x1 (Sing x2))), λ x3 . lam 2 (λ x4 . If_i (x4 = 0) (ap x3 x2) (lam (setminus x1 (Sing x2)) (λ x5 . ap x3 x5))).

Apply unknownprop_aa42ade5598d8612d2029318c4ed81646c550ecc6cdd9ab953ce4bf73f3dd562 with setexp x0 x1, setprod x0 (setexp x0 (setminus x1 (Sing x2))), λ x3 . lam 2 (λ x4 . If_i (x4 = 0) (ap x3 x2) (lam (setminus x1 (Sing x2)) (λ x5 . ap x3 x5))) leaving 2 subgoals.

Apply unknownprop_57c8600e4bc6abecef2ae17962906fa2de1fc16f5d46ed100ff99cd5b67f5b1b with setexp x0 x1, setprod x0 (setexp x0 (setminus x1 (Sing x2))), λ x3 . lam 2 (λ x4 . If_i (x4 = 0) (ap x3 x2) (lam (setminus x1 (Sing x2)) (λ x5 . ap x3 x5))) leaving 2 subgoals.

Let x3 of type ι be given.

Assume H1: In x3 (setexp x0 x1).

Apply unknownprop_ca2474a6276e8f820c97f5b2341436efc5ee69afd93bd4fd7a8b330e27b79018 with x0, setexp x0 (setminus x1 (Sing x2)), ap x3 x2, lam (setminus x1 (Sing x2)) (λ x4 . ap x3 x4) leaving 2 subgoals.

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

The subproof is completed by applying H1.

The subproof is completed by applying H0.

Apply unknownprop_204aaff43997dfdee1bf2ffda080faf1153e7eb6d169528444a836fe2ecc543c with setminus x1 (Sing x2), x0, λ x4 . ap x3 x4.

Let x4 of type ι be given.

Assume H2: In x4 (setminus x1 (Sing x2)).

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

The subproof is completed by applying H1.

Apply unknownprop_29bb348fa91dd336b68009f32eb9809a20ab7c7920c130047ad13aae3b335ac5 with x1, Sing x2, x4.

The subproof is completed by applying H2.

Let x3 of type ι be given.

Assume H1: In x3 (setexp x0 x1).

Let x4 of type ι be given.

Assume H2: In x4 (setexp x0 x1).

Assume H3: (λ x5 . lam 2 (λ x6 . If_i (x6 = 0) (ap x5 x2) (lam (setminus x1 (Sing x2)) (λ x7 . ap x5 x7)))) x3 = (λ x5 . lam 2 (λ x6 . If_i (x6 = 0) (ap x5 x2) (lam (setminus x1 (Sing x2)) (λ x7 . ap x5 x7)))) x4.

Apply unknownprop_89c61d8efbfed10cda65f88aa560c75c9a07b94af4fe272148bd98e7547600ec with ap x3 x2, lam (setminus x1 (Sing x2)) (λ x5 . ap x3 x5), ap x4 x2, lam (setminus x1 (Sing x2)) (λ x5 . ap x4 x5), x3 = x4 leaving 2 subgoals.

The subproof is completed by applying H3.

Assume H4: ap x3 x2 = ap x4 x2.

Assume H5: lam (setminus x1 (Sing x2)) (ap x3) = lam (setminus x1 (Sing x2)) (ap x4).

Apply unknownprop_23208921203993e7c79234f69a10e3d42c3011a560c83fb48a9d1a8f3b50675c with x1, x0, x3, x4 leaving 3 subgoals.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

Let x5 of type ι be given.

Assume H6: In ... ....

...

■

Proofgold Proof