Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_3069c6fa8dbd033f1c94555c93d580ac5c2fd979807cb20dbdb8dc4cc9b1517f with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_077979b790f9097ea9250573e60509ec9410103c35a67e0558983ee18582fb09 with
x2.
The subproof is completed by applying H2.
Apply unknownprop_dd5df7669a233e3d5e134397e0a0943dece6dcd81d988e2d3c963c02c7bcf901 with
ordsucc x2,
x1,
λ x3 x4 . In x4 (mul_nat (ordsucc x2) x0) leaving 3 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L3.
Apply unknownprop_dd5df7669a233e3d5e134397e0a0943dece6dcd81d988e2d3c963c02c7bcf901 with
ordsucc x2,
x0,
λ x3 x4 . In (mul_nat x1 (ordsucc x2)) x4 leaving 3 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying H0.
Apply unknownprop_f7683dc714ad1679ffb6b54fdd5b814a276d9a69b85d4456dbb9f3586b3efa7f with
x0,
x1,
x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.