Avoid bottomify-ing higher order functions

Reworked value type to more closely match the possible spec.

Deduplicated `interp_ident` / `abstract_interp_ident` overlapped state.

The specification of `reify` and `reflect` has been simplified to more
closely match the intuition: `reify`'s spec no longer talks about output
bounds, only interpretation, and a companion lemma
`abstraction_relation_of_related_bounded_value'` shows that the spec of
`reflect` is effectively one direction of an isomorphism between
interpreted-values bounded by abstract state, and `value`s which are in
relationship with the given interpreted-value.  Not really sure how best
to describe this in words yet, probably needs some digesting work.

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).

Author: JasonGross