Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H0: equip x0 (ordsucc x3).

Assume H1: equip x1 x3.

Claim L2: ...

...

Apply unknownprop_607e36a92fe018510c0fe37088a293d37baaa001ac433e03d9364730e0ca1993 with x0, x1, x2, 1, x2 leaving 2 subgoals.

Apply unknownprop_01b7f7993ff222473c0dc551f861729864a2fa847d49dc4751edad0602198144 with setsum x1 1, ordsucc x3, x0 leaving 2 subgoals.

Apply unknownprop_1b764290fde7c6be5dad24a6a257b6d0c773613bb687261020b529743ed07853 with ordsucc x3, setsum x1 1.

Apply unknownprop_f82d0f217e1b2a36bc273d145ee21e9b9e753d654bb0c650cc08860c1b4bd1f0 with x3, x1, equip (ordsucc x3) (setsum x1 1) leaving 2 subgoals.

Apply unknownprop_1b764290fde7c6be5dad24a6a257b6d0c773613bb687261020b529743ed07853 with x1, x3.

The subproof is completed by applying H1.

Let x4 of type ι → ι be given.

Assume H3: bij x3 x1 x4.

Apply unknownprop_db24d9aa1dc52b3c0eaf7cf69655226164a8ab5afc5d72e14a32016133f537ca with x3, x1, x4, equip (ordsucc x3) (setsum x1 1) leaving 2 subgoals.

The subproof is completed by applying H3.

Assume H4: inj x3 x1 x4.

Assume H5: ∀ x5 . In x5 x1 ⟶ ∃ x6 . and (In x6 x3) (x4 x6 = x5).

Apply unknownprop_6a8f953ba7c3bf327e583b76a91b24ddd499843a498fbfe2514e26f3800e68b3 with x3, x1, x4, equip (ordsucc x3) (setsum x1 1) leaving 2 subgoals.

The subproof is completed by applying H4.

Assume H6: ∀ x5 . In x5 x3 ⟶ In (x4 x5) x1.

Assume H7: ∀ x5 . In x5 x3 ⟶ ∀ x6 . In x6 x3 ⟶ x4 x5 = x4 x6 ⟶ x5 = x6.

Apply unknownprop_4b95783dcb3eee1943e1de5542f675166ef402c8fbdda80bdf0920b55d3fc6de with ordsucc x3, setsum x1 1, λ x5 . If_i (In x5 x3) (Inj0 (x4 x5)) (Inj1 0).

Apply unknownprop_aa42ade5598d8612d2029318c4ed81646c550ecc6cdd9ab953ce4bf73f3dd562 with ordsucc x3, setsum x1 1, λ x5 . If_i (In x5 x3) (Inj0 (x4 x5)) (Inj1 0) leaving 2 subgoals.

Apply unknownprop_57c8600e4bc6abecef2ae17962906fa2de1fc16f5d46ed100ff99cd5b67f5b1b with ordsucc x3, setsum x1 1, λ x5 . If_i (In x5 x3) (Inj0 (x4 x5)) (Inj1 0) leaving 2 subgoals.

Let x5 of type ι be given.

Assume H8: In x5 (ordsucc x3).

Apply unknownprop_84fe37a922385756a4e0826a593defb788cadbe4bdc9a7fe6b519ea49f509df5 with x3, x5, In (If_i (In x5 x3) (Inj0 (x4 x5)) (Inj1 0)) (setsum x1 1) leaving 3 subgoals.

The subproof is completed by applying H8.

Assume H9: In x5 x3.

Apply unknownprop_6f44febdf8a865ee94133af873e3c2941a931de6ac80968301360290e02ca608 with In x5 x3, Inj0 (x4 x5), Inj1 0, λ x6 x7 . In x7 (setsum x1 1) leaving 2 subgoals.

The subproof is completed by applying H9.

Apply unknownprop_1fbfebc9584f3b35fe974f93c7762fab1d5a4f649af5608ad307cbbc36ce4d37 with x1, 1, x4 x5.

Apply H6 with x5.

The subproof is completed by applying H9.

Assume H9: x5 = x3.

Apply H9 with λ x6 x7 . In (If_i (In x7 x3) (Inj0 (x4 x7)) (Inj1 0)) (setsum x1 1).

Apply unknownprop_5a150bd86f4285de5d98c60b17d4452a655b4d88de0a02247259cdad6e6d992c with In x3 x3, Inj0 (x4 x3), Inj1 0, λ x6 x7 . In x7 (setsum x1 1) leaving 2 subgoals.

The subproof is completed by applying L2.

Apply unknownprop_509aadde20bd8e655e679e36fea278577d08a1dbe475eed73f3fccc8c2d65f15 with x1, 1, 0.

The subproof is completed by applying unknownprop_b28daf094ddd549776d741eec1dac894d28f0f162bae7bdbdbfb7366b31cdef0.

Let x5 of type ι be given.

Assume H8: In x5 (ordsucc x3).

Let x6 of type ι be given.

Assume H9: In x6 (ordsucc x3).

Apply unknownprop_84fe37a922385756a4e0826a593defb788cadbe4bdc9a7fe6b519ea49f509df5 with x3, x5, If_i (In x5 x3) (Inj0 (x4 x5)) (Inj1 0) = If_i (In x6 x3) (Inj0 (x4 x6)) (Inj1 0) ⟶ x5 = x6 leaving 3 subgoals.

The subproof is completed by applying H8.

Assume H10: In x5 x3.

Apply unknownprop_6f44febdf8a865ee94133af873e3c2941a931de6ac80968301360290e02ca608 with In x5 x3, ..., ..., ... leaving 2 subgoals.

...

■

Proofgold Proof