I was coming to say almost the exact opposite. `ToBytes(0)` should be equal to the empty array. This seems like the more natural representation, at least to m

I was coming to say almost the exact opposite. `ToBytes(0)` should be equal to the empty array. This seems like the more natural representation, at least to me. 1. The implementation of `FromBytes` works properly only if the base case returns 0 for the empty array. So you already have, for free, `FromBytes([]) == 0`. You might as well use it. 2. `LemmaFromToBytes` currently requires the somewhat awkward and complicated `requires |bytes| > 0 && (|bytes| == 1 || bytes[0] != 0)`. We need to restrict this to only allowing non-empty arrays. And then we need to restrict it to not allowing leading zeros on arrays, except if the array is of length 1 and then we do allow a leading zero. If we represent 0 as `[]` instead of `[0]` then this all simplifies down to something like `requires |bytes| == 0 || bytes[0] != 0`. We allow arrays of any size and we never allow leading zeros on any array, which is easier to express. 3. Currently `ToBytes` has an `if-else` at the end and requires repeating the code `[byte]` in both branches. That's obviously not a lot of repetition but wouldn't it be nice to eliminate that? If we change the beginning to `if v == 0 then []` then we can replace the `if-else` at the end with just `ToBytes(w) + [byte]`. And we can get rid of the `ensures |r| > 0`. Then the structure of `ToBytes` and `FromBytes` more closely mirror each other, with the base cases being "the same".