Apply unknownprop_e9c4cec7fb327dcb17b88acdaf76daee024e49fa71834a13065f86e12e958609 with
u2,
u5,
λ x0 x1 . x1 = u64 leaving 2 subgoals.
The subproof is completed by applying nat_5.
Apply unknownprop_8e67f22739f9a01fd2d9438edd2f3f6d8d323d1fa4d050bc09f5b1af8d3b6dd7 with
λ x0 x1 . mul_nat u2 x1 = u64.
Apply unknownprop_463ff37e0f5b1f0c9f9e5bd24ebf02eb01188a79277f3c1f714af19504beaaf2 with
u32,
λ x0 x1 . x1 = u64 leaving 2 subgoals.
The subproof is completed by applying unknownprop_e20297641bb65d9e51ebac2e053948365a3f53b65d223d41920ce90b2e26b533.
The subproof is completed by applying unknownprop_a34b3c5959e47d7a872d45ff0bb955b2395f68e02845b109079692e68f980757.