Let x0 of type ι be given.

Let x1 of type ι be given.

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

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

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

Let x2 of type ι be given.

Assume H0: In x2 (setexp x1 (ordsucc x0)).

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

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

The subproof is completed by applying H0.

The subproof is completed by applying unknownprop_4b3850b342b3607d712ced4e4c9fa37dbdc70692760e3dc82f8fd86e9b26a6b5 with x0.

Apply unknownprop_204aaff43997dfdee1bf2ffda080faf1153e7eb6d169528444a836fe2ecc543c with x0, x1, λ x3 . ap x2 x3.

Let x3 of type ι be given.

Assume H1: In x3 x0.

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

The subproof is completed by applying H0.

Apply unknownprop_9d1f2833af10907d78259d2045ff2d1e1026643f459cca4199c4ae7f89385ba4 with x0, x3.

The subproof is completed by applying H1.

Let x2 of type ι be given.

Assume H0: In x2 (setexp x1 (ordsucc x0)).

Let x3 of type ι be given.

Assume H1: In x3 (setexp x1 (ordsucc x0)).

Assume H2: (λ x4 . lam 2 (λ x5 . If_i (x5 = 0) (ap x4 x0) (lam x0 (λ x6 . ap x4 x6)))) x2 = (λ x4 . lam 2 (λ x5 . If_i (x5 = 0) (ap x4 x0) (lam x0 (λ x6 . ap x4 x6)))) x3.

Apply unknownprop_89c61d8efbfed10cda65f88aa560c75c9a07b94af4fe272148bd98e7547600ec with ap x2 x0, lam x0 (λ x4 . ap x2 x4), ap x3 x0, lam x0 (λ x4 . ap x3 x4), x2 = x3 leaving 2 subgoals.

The subproof is completed by applying H2.

Assume H3: ap x2 x0 = ap x3 x0.

Assume H4: lam x0 (ap x2) = lam x0 (ap x3).

Apply unknownprop_23208921203993e7c79234f69a10e3d42c3011a560c83fb48a9d1a8f3b50675c with ordsucc x0, x1, x2, x3 leaving 3 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

Let x4 of type ι be given.

Assume H5: In x4 (ordsucc x0).

Apply unknownprop_84fe37a922385756a4e0826a593defb788cadbe4bdc9a7fe6b519ea49f509df5 with x0, x4, ap x2 x4 = ap x3 x4 leaving 3 subgoals.

The subproof is completed by applying H5.

Assume H6: In x4 x0.

Apply unknownprop_c5e2164052a280ad5b04f622e53815f0267ee33361e4345305e43303abef2c1b with x0, λ x5 . ap x2 x5, x4, λ x5 x6 . x5 = ap x3 x4 leaving 2 subgoals.

The subproof is completed by applying H6.

Apply unknownprop_c5e2164052a280ad5b04f622e53815f0267ee33361e4345305e43303abef2c1b with x0, λ x5 . ap x3 x5, x4, λ x5 x6 . ap (lam x0 (ap x2)) x4 = x5 leaving 2 subgoals.

The subproof is completed by applying H6.

Apply H4 with λ x5 x6 . ap x6 x4 = ap ... ....

...

■

Proofgold Proof