Let x0 of type ι be given.
Apply unknownprop_01b7f7993ff222473c0dc551f861729864a2fa847d49dc4751edad0602198144 with
Power x0,
setexp 2 x0,
2 leaving 2 subgoals.
Apply unknownprop_1b764290fde7c6be5dad24a6a257b6d0c773613bb687261020b529743ed07853 with
setexp 2 x0,
Power x0.
The subproof is completed by applying unknownprop_ea7b2e6e9976e1e45c4370d74dce7d59ce8c101b4763ea3138e546088f666e00 with x0.
Apply unknownprop_f1b4b3f3609f7bbf0bc8735b08d44bfebb6a6346e99882a47fb54ee009e3ab08 with
λ x1 x2 . equip (setexp 2 x0) x1.
Apply unknownprop_23bcce9de27917b36a2eb3896bbcf9b010d077f8f71bb6ef8f541b742d24258c with
2,
1,
2,
x0 leaving 4 subgoals.
The subproof is completed by applying unknownprop_d97d6922f54612bc34684069408098060ad6c1b04a8b4fda7efccfad8c5e25b7.
The subproof is completed by applying unknownprop_8d353ccfb170ea018406af7266d499508cf5be2cebcac5c8a89ccd16a50d0251.
The subproof is completed by applying unknownprop_779bad135e02b130c4f2c6fb2f6a4cc60941e04327d78e3212c24d54199ba5e5 with 2.
The subproof is completed by applying H0.