Minor polishing of MWHILE proofs.