Refinements and fixes per F* call yesterday.
  Sorry for earlier sloppiness.