Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι be given.
Let x6 of type ι be given.
Let x7 of type ι be given.
Apply atleastp_tra with
SetAdjoin (SetAdjoin (SetAdjoin (SetAdjoin (SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3) x4) x5) x6) x7,
setsum u7 u1,
u8 leaving 2 subgoals.
Apply unknownprop_8805a75f81012de0423e9173532fc074fb73b80e451597fde52287a4721fb204 with
SetAdjoin (SetAdjoin (SetAdjoin (SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3) x4) x5) x6,
Sing x7,
u7,
u1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_e3d792208a43699ac881369daf980df8fc1c9033274e154dfa581ec0b9f01408 with x0, x1, x2, x3, x4, x5, x6.
The subproof is completed by applying unknownprop_6f4f3b954cb736651074754cd4a7a9c9f8fdee5b2d9e8c774389a322e59d45f1 with x7.
Apply equip_atleastp with
setsum u7 u1,
ordsucc u7.
Apply equip_sym with
ordsucc u7,
setsum u7 u1.
Apply unknownprop_d631a7130d5b5dc7c63be4f6ec657039b3370cb84697eaa2bc8ab827ff606adf with
u7,
λ x8 x9 . equip x8 (setsum u7 u1).
Apply unknownprop_80fb4e499c5b9d344e7e79a37790e81cc16e6fd6cd87e88e961f3c8c4d6d418f with
u7,
u1,
u7,
u1 leaving 4 subgoals.
The subproof is completed by applying nat_7.
The subproof is completed by applying nat_1.
The subproof is completed by applying equip_ref with
u7.
The subproof is completed by applying equip_ref with
u1.