Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_01b7f7993ff222473c0dc551f861729864a2fa847d49dc4751edad0602198144 with
setexp x1 3,
setprod x1 (setexp x1 2),
69aae.. x0 3 leaving 2 subgoals.
The subproof is completed by applying unknownprop_3b47c6401014a05d6eff219109a6fab7915845fcaa33666aa5b7d69b07f28a1c with 2, x1.
Apply unknownprop_adc51df32e37a02ae01a7627d71f293cbf548824fcf0d70ccbf318430642e27c with
x0,
2,
λ x2 x3 . equip (setprod x1 (setexp x1 2)) x3 leaving 2 subgoals.
The subproof is completed by applying unknownprop_d97d6922f54612bc34684069408098060ad6c1b04a8b4fda7efccfad8c5e25b7.
Apply unknownprop_b8fbbba1527cbd64146da68212d93c3041b26e632212bb254ebdd564a5aa3700 with
x0,
69aae.. x0 2,
x1,
setexp x1 2 leaving 4 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_daf12a89807432f888a9e8d9f945f19a550f6522b3809f1046e786c0b50b4322 with
x0,
2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_d97d6922f54612bc34684069408098060ad6c1b04a8b4fda7efccfad8c5e25b7.
The subproof is completed by applying H1.
Apply unknownprop_f75c24c238ad21185786122172338a9cbfd0e686556021ad10ec75e3ddb12897 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.