Added comment about ease of proof in abstract, because POPL.