Apply unknownprop_f23dde3020cfe827bdc4db0338b279dd2c0f6c90742a195a1a7a614475669076 with
λ x0 . ∃ x1 . and (nat_p x1) (equip (V_ x0) x1) leaving 2 subgoals.
Let x0 of type ο be given.
Apply H0 with
0.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
nat_p 0,
equip (V_ 0) 0 leaving 2 subgoals.
The subproof is completed by applying unknownprop_0e150139fedb8d7a0ae85e3054b4c73c936e7acb880ce730fb00a0093c9c6c27.
Apply unknownprop_fa1d3a4a00c90be7720377aeb98583e9ec1104c7f9b8661e216ae25581a1e970 with
λ x1 x2 . equip x2 0.
The subproof is completed by applying unknownprop_779bad135e02b130c4f2c6fb2f6a4cc60941e04327d78e3212c24d54199ba5e5 with 0.
Let x0 of type ι be given.
Apply H1 with
∃ x1 . and (nat_p x1) (equip (V_ (ordsucc x0)) x1).
Let x1 of type ι be given.
Apply andE with
nat_p x1,
equip (V_ x0) x1,
∃ x2 . and (nat_p x2) (equip (V_ (ordsucc x0)) x2) leaving 2 subgoals.
The subproof is completed by applying H2.
Let x2 of type ο be given.
Apply H5 with
69aae.. 2 x1.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
nat_p (69aae.. 2 x1),
equip (V_ (ordsucc x0)) (69aae.. 2 x1) leaving 2 subgoals.
Apply unknownprop_daf12a89807432f888a9e8d9f945f19a550f6522b3809f1046e786c0b50b4322 with
2,
x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_d97d6922f54612bc34684069408098060ad6c1b04a8b4fda7efccfad8c5e25b7.
The subproof is completed by applying H3.
Apply unknownprop_23bd0988c177927f99f51fb764bb0f8ea4175a3b8648d03025af2bff9cf62626 with
x0,
λ x3 x4 . equip x4 (69aae.. 2 x1) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_01b7f7993ff222473c0dc551f861729864a2fa847d49dc4751edad0602198144 with
Power (V_ x0),
setexp 2 x1,
69aae.. 2 x1 leaving 2 subgoals.
Apply unknownprop_fd9de64ecc38eca3f97f7d4396a1f520052343c0ee907cdc39e13077655a4063 with
V_ x0,
x1.
The subproof is completed by applying H4.
Apply unknownprop_8c007fc18718b3c11de57e78a99458b005cd25fec9b21b7ad884fb715186d0af with
2,
x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_d97d6922f54612bc34684069408098060ad6c1b04a8b4fda7efccfad8c5e25b7.
The subproof is completed by applying H3.