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