Prove a Hoare-like rule for FOR, and use it in a few proofs.

It causes much pain when attempting results of the form

  FOR (lo,hi) ... = FOR (lo,hi) ...

though. Easier in this circumstance to just induct on `hi - lo`.