Apply unknownprop_f23dde3020cfe827bdc4db0338b279dd2c0f6c90742a195a1a7a614475669076 with
λ x0 . ∀ x1 . Subq x1 x0 ⟶ ∃ x2 . and (In x2 (ordsucc x0)) (equip x1 x2) leaving 2 subgoals.
Let x0 of type ι be given.
Let x1 of type ο be given.
Assume H1:
∀ x2 . and (In x2 1) (equip x0 x2) ⟶ x1.
Apply H1 with
0.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
In 0 1,
equip x0 0 leaving 2 subgoals.
The subproof is completed by applying unknownprop_b28daf094ddd549776d741eec1dac894d28f0f162bae7bdbdbfb7366b31cdef0.
Claim L2: x0 = 0
Apply unknownprop_73b312e5c0ced1987581817c61d2a6ab9e4c47a87f99557a6b2723117244e7d9 with
x0.
The subproof is completed by applying H0.
Apply L2 with
λ x2 x3 . equip x3 0.
The subproof is completed by applying unknownprop_779bad135e02b130c4f2c6fb2f6a4cc60941e04327d78e3212c24d54199ba5e5 with 0.
Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_80056f9db85f84f8ce0644e1cdb62f5e66ec62c041f28dd7a07b3c46de1ea696 with
x0,
x1,
∃ x2 . and (In x2 (ordsucc (ordsucc x0))) (equip x1 x2) leaving 2 subgoals.
Apply H1 with
setminus x1 (Sing x0),
∃ x2 . and (In x2 (ordsucc (ordsucc x0))) (equip x1 x2) leaving 2 subgoals.
The subproof is completed by applying L4.
Let x2 of type ι be given.
Apply andE with
In x2 (ordsucc x0),
equip (setminus x1 (Sing x0)) x2,
∃ x3 . and (In x3 (ordsucc (ordsucc x0))) (equip x1 x3) leaving 2 subgoals.
The subproof is completed by applying H5.
Apply unknownprop_077979b790f9097ea9250573e60509ec9410103c35a67e0558983ee18582fb09 with
x0.
The subproof is completed by applying H0.
Apply unknownprop_3069c6fa8dbd033f1c94555c93d580ac5c2fd979807cb20dbdb8dc4cc9b1517f with
ordsucc x0,
x2 leaving 2 subgoals.
The subproof is completed by applying L8.
The subproof is completed by applying H6.
Let x3 of type ο be given.
Apply H10 with
ordsucc x2.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
In (ordsucc x2) (ordsucc (ordsucc x0)),
equip x1 (ordsucc x2) leaving 2 subgoals.
Apply unknownprop_a8f766a07ce4037c1a1cdb7512a4eb008ff74917c7385d889b7b933b3b099900 with
ordsucc x0,
x2 leaving 2 subgoals.
The subproof is completed by applying L8.
The subproof is completed by applying H6.
Apply unknownprop_01b7f7993ff222473c0dc551f861729864a2fa847d49dc4751edad0602198144 with
x1,
setsum (Sing x0) (setminus x1 (Sing x0)),
ordsucc x2 leaving 2 subgoals.
Apply unknownprop_1b764290fde7c6be5dad24a6a257b6d0c773613bb687261020b529743ed07853 with
setsum (Sing x0) (setminus x1 (Sing x0)),
x1.
Apply unknownprop_90a352f74f9892bfc39c1ccdaecae19d23018050a6f899381839d73f3a3293bc with
x1,
Sing x0.
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
Sing x0,
x1.
Let x4 of type ι be given.
Apply unknownprop_5b60b98e3f1eb090f9a13c5f00bc0b9619444831e46991a07d9b3c034c70e912 with
x0,
x4,
λ x5 x6 . In x6 x1 leaving 2 subgoals.
The subproof is completed by applying H11.
The subproof is completed by applying H3.
Apply unknownprop_0f2aa9b9aed91abb437bf5f1810ffadef0d49105ca48481c9364781077821ad5 with
x2,
λ x4 x5 . equip (setsum (Sing x0) (setminus x1 (Sing x0))) x5.
Apply unknownprop_0bc05861c326df1bc856e9663c3bd091fe6729155095d255366b172bf07600be with
x2,
1,
λ x4 x5 . equip (setsum (Sing x0) (setminus x1 (Sing x0))) x5 leaving 3 subgoals.
The subproof is completed by applying L9.
The subproof is completed by applying unknownprop_8d353ccfb170ea018406af7266d499508cf5be2cebcac5c8a89ccd16a50d0251.
Apply unknownprop_10a8359a9f4efa213440b7ef6df64889edc029a3e3c945886df91a6694ff6c71 with
1,
x2,
Sing x0,
setminus x1 (Sing x0) leaving 4 subgoals.
The subproof is completed by applying unknownprop_8d353ccfb170ea018406af7266d499508cf5be2cebcac5c8a89ccd16a50d0251.
The subproof is completed by applying L9.
The subproof is completed by applying unknownprop_b28fcc1d004191675839613f2da0a58a0048f9c1b3a3a0dafee7400c04be0317 with x0.
The subproof is completed by applying H7.