Rework expression inference spec draft based on review comments. (#3850)

The following changes (mostly based on suggestions by Leaf and Erik)
are included:

- The text is now under a heading called "expression inference" rather
  than "body inference" (which was confusing).

- Instead of trying to describe the output of type inference using a
  vague notion of "expression artifacts" whose runtime behavior is
  described in prose, I'm specifying it using a Dart-like syntax
  called "elaborated expressions". Elaborated expressions look
  generally like Dart expressions, except they have some limitations
  (types are fully specified, and complex constructs like null
  shorting are desugared, and type checks are explicit) and support
  some extra forms (such as "let" expressions).

- I've simplified the terminology I use to describe the three things
  that can happen when an expression is evaluated (it can diverge,
  throw an exception, or evaluate to a value). My previous terminology
  was confusing ("fail to complete at all", "complete normally with a
  value", or "complete with an exception").

- I've re-worked the treatment coercions so that I'm no longer making
  subsumption explicit in the language of elaborated expressions. (I
  never meant to make subsumption explicit; it happened as a mistake
  due to unclear thinking on my part.)

- I broke the "numbers" subsection into separate "integer literals"
  and "double literals" sections. (Previosuly I only specified how
  integer literals are handled.)

- The sketches of soundness proofs have been simplified a bit. I'm no
  longer trying to crisply distinguish "expression soundness", "return
  value soundness", "tear-off soundness", and "future soundness";
  rather, I'm speaking about soundness more informally, as befits an
  informal proof sketch.

- On the other hand, I've clarified precisely what I mean by "is an
  instance of", since the soundness proof sketches don't make any
  sense if your definition of this concept doesn't agree with what's
  in my head. I've also made sure this concept correctly accounts for
  extension types.

- And I've added text explaining why the interpretation of `await`
  expressions is indeed sound. (Previously I had a "TODO" because I
  thought maybe they weren't sound. But they're sound; it just took a
  little extra work to prove it to myself.)