Let x0 of type ι be given.
Apply unknownprop_7ee30a400cfd424043a758aab31c2f0618cf50b5494b887b1daa7c210d8b669c with
x0,
∃ x1 . and (nat_p x1) (equip x0 x1).
Let x1 of type ι be given.
Apply andE with
nat_p x1,
Subq x0 (V_ x1),
∃ x2 . and (nat_p x2) (equip x0 x2) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_e5301b3d70bda0519d63620f3030249cd4bf7b92497d8242491e59897566ec4b with
x1,
∃ x2 . and (nat_p x2) (equip x0 x2) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Apply andE with
nat_p x2,
equip (V_ x1) x2,
∃ x3 . and (nat_p x3) (equip x0 x3) leaving 2 subgoals.
The subproof is completed by applying H3.
Apply unknownprop_1e700568a0dea83e9205b92030c70aa9826d35a7d4d34d0c09146e12a302186c with
x0,
V_ x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_b5d0a0123c3a8bc9dcc2915dc24ee4bb0a510635f6946e2a5486e14fe0d606b6 with
V_ x1,
x2.
The subproof is completed by applying H5.
Apply unknownprop_a9f44ec091e6d0adbe4c16f839b6f21aca2f69b01c4c17b7bf5421317efb2f00 with
x0,
x2,
∃ x3 . and (nat_p x3) (equip x0 x3) leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying L6.
Let x3 of type ι be given.
Apply andE with
In x3 (ordsucc x2),
equip x0 x3,
∃ x4 . and (nat_p x4) (equip x0 x4) leaving 2 subgoals.
The subproof is completed by applying H7.
Let x4 of type ο be given.
Apply H10 with
x3.
Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with
nat_p x3,
equip x0 x3 leaving 2 subgoals.
Apply unknownprop_3069c6fa8dbd033f1c94555c93d580ac5c2fd979807cb20dbdb8dc4cc9b1517f with
ordsucc x2,
x3 leaving 2 subgoals.
Apply unknownprop_077979b790f9097ea9250573e60509ec9410103c35a67e0558983ee18582fb09 with
x2.
The subproof is completed by applying H4.
The subproof is completed by applying H8.
The subproof is completed by applying H9.