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