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