Avoid bottomify-ing higher order functions

Reworked value type to more closely match the possible spec.

Deduplicated `interp_ident` / `abstract_interp_ident` overlapped state.

There's some interesting lemmas where we have an equivalency between two
ways of representing things only for up-to-second-order types, and an
implication for up-to-third-order types, which is currently all the
identifiers.  But this means that if we add fourth-order identifiers,
we'll have to deal with two different sorts of `Proper` abstraction
relations (one used by `Assembly/Symbolic` and one used by bounds
analysis, though it's possible the `Assembly/Symbolic` one can be
adapted).