more compiler proof fixes
finish updating compiler proofs