Minor update to ASM proof for x86-64.

Use some lemmas to speed up a proof.