Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_01b7f7993ff222473c0dc551f861729864a2fa847d49dc4751edad0602198144 with
Power x0,
Power x1,
setexp 2 x1 leaving 2 subgoals.
Apply unknownprop_cd671c8fea33cd6003f9577dac7db4095d190ad88305992deb1ba8aabb57c424 with
x0,
x1.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_aa80dfb41e76eeaa5d473a9f2e5e58d879a0b7409cd505d3df670582d7a9ee0d with x1.