fix semantics of abstractions, and reduce semantics_raconv to one cheat

For abstractions, I have a function that picks the semantics of the body
given the semantics of the argument. This needs only pick a good set for
things in the domain type, and needs to produce something in the range
type. Updated the semantics to specify those conditions. This has
knock-on effects on all the proofs so far, whose statements have
slightly changed... mostly they got weaker, but in ways that look
harmless.