More work on proofs in ScanState.v