Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply unknownprop_fc3f08095f77ec388b89b48e2b52040a80a894c58ae8421f993dbbc015fb91c5 with
λ x4 x5 : ι → ι → ι . equip (x5 x2 x3) (add_nat x0 (69aae.. 2 x1)).
Apply unknownprop_10a8359a9f4efa213440b7ef6df64889edc029a3e3c945886df91a6694ff6c71 with
x0,
69aae.. 2 x1,
x2,
Power x3 leaving 4 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_daf12a89807432f888a9e8d9f945f19a550f6522b3809f1046e786c0b50b4322 with
2,
x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_d97d6922f54612bc34684069408098060ad6c1b04a8b4fda7efccfad8c5e25b7.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_01b7f7993ff222473c0dc551f861729864a2fa847d49dc4751edad0602198144 with
Power x3,
setexp 2 x3,
69aae.. 2 x1 leaving 2 subgoals.
Apply unknownprop_1b764290fde7c6be5dad24a6a257b6d0c773613bb687261020b529743ed07853 with
setexp 2 x3,
Power x3.
The subproof is completed by applying unknownprop_ea7b2e6e9976e1e45c4370d74dce7d59ce8c101b4763ea3138e546088f666e00 with x3.
Apply unknownprop_23bcce9de27917b36a2eb3896bbcf9b010d077f8f71bb6ef8f541b742d24258c with
2,
x1,
2,
x3 leaving 4 subgoals.
The subproof is completed by applying unknownprop_d97d6922f54612bc34684069408098060ad6c1b04a8b4fda7efccfad8c5e25b7.
The subproof is completed by applying H1.
The subproof is completed by applying unknownprop_779bad135e02b130c4f2c6fb2f6a4cc60941e04327d78e3212c24d54199ba5e5 with 2.
The subproof is completed by applying H3.