Let x0 of type ι be given.
Apply unknownprop_f23dde3020cfe827bdc4db0338b279dd2c0f6c90742a195a1a7a614475669076 with
λ x1 . equip (setexp x0 x1) (69aae.. x0 x1) leaving 2 subgoals.
Apply unknownprop_4ef67fc5b8b30ebc0b691020299a978fd97f9ab288d7f37b768f51bf86e2a3c3 with
x0,
λ x1 x2 . equip (setexp x0 0) x2.
Apply unknownprop_443f0b3f0997d6514ee15619d5b7b607e3c37b74f373515a6873fe72e102cd0b with
x0,
λ x1 x2 . equip x2 1.
The subproof is completed by applying unknownprop_779bad135e02b130c4f2c6fb2f6a4cc60941e04327d78e3212c24d54199ba5e5 with 1.
Let x1 of type ι be given.
Apply unknownprop_daf12a89807432f888a9e8d9f945f19a550f6522b3809f1046e786c0b50b4322 with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_adc51df32e37a02ae01a7627d71f293cbf548824fcf0d70ccbf318430642e27c with
x0,
x1,
λ x2 x3 . equip (setexp x0 (ordsucc x1)) x3 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_dd5df7669a233e3d5e134397e0a0943dece6dcd81d988e2d3c963c02c7bcf901 with
x0,
69aae.. x0 x1,
λ x2 x3 . equip (setexp x0 (ordsucc x1)) x3 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
Apply unknownprop_01b7f7993ff222473c0dc551f861729864a2fa847d49dc4751edad0602198144 with
setexp x0 (ordsucc x1),
setprod (setexp x0 x1) x0,
mul_nat (69aae.. x0 x1) x0 leaving 2 subgoals.
The subproof is completed by applying unknownprop_1e876b7e1fb67bb7f01c72f3f9cc106d21772f3f19695c438d33f53e9e7a73eb with x0, x1.
Apply unknownprop_b8fbbba1527cbd64146da68212d93c3041b26e632212bb254ebdd564a5aa3700 with
69aae.. x0 x1,
x0,
setexp x0 x1,
x0 leaving 4 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying unknownprop_779bad135e02b130c4f2c6fb2f6a4cc60941e04327d78e3212c24d54199ba5e5 with x0.