Remove constants for word32, word64, word128

[JasonGross]

Currently there's a decent amount of code in src/Util/FixedWordSizes.v and src/Util/FixedWordSizesEquality.v that allows us to have separate word32, word64, and word128 constants without treating those cases specially when we use them. We did this so we could extract them to separate things. In the new refinement-based system, do we want to keep them (there is minimal additional cost incurred in keeping them), or do we want to strip them out and have less code, possibly as part of #14?

(The most important thing in the short term is to be consistent about which notion of word we're using.)

[andres-erbsen]

I thought we were going to use { z:Z | 0 <= z < 2^64 } as the word type for some reason you cared about. Either way, I dont think we need these definitions anymore. Independently, I think we might later want to support arbitrary types that behave like { z:Z | A <= z < B } for some A and B, but let's see about that when we get there.

[JasonGross]

I think we should leave this open as a reminder, possibly renaming it; I'm going to prioritize finishing the admitted proofs and integration over removing this code.

[JasonGross]

This will be closed once we switch over to the new pipeline from #373.