Added file headers to *_Properties.v
Removed old comments.
Added more target theorems, with proof sketches.