Use toNat to avoid %assert_total when negative Int is treated the same as 0.
Replace some Heap proofs with impossible.