Make sure allocation theorems actually apply after [simpl]

[tchajed]

The various allocation methods (ref, ref_to, NewSlice, NewMap) sometimes get unfolded and then the nice typed theorems about them don't apply. We should make sure they use opaque representations which are values (in some cases they were incorrectly made expressions, which have to be simplified to substitute through them).