transformation correctness

[Stephen Weeks]

Neal reasonably objected to the following statement in the introduction

  We define a condition on analyses that guarantees the correctness of the
  transformation. 

since we never even state, let alone prove, a correctness theorem in 4.2.  Since 
we don't do so, and haven't really thought about it, I'm inclined to drop the
sentence.

It would be nice to have something about correctness (and type correctness) of
the transformation, but I haven't thought about it enough to feel comfortable
saying anything.