Make permutability proofs more concise.

And, honestly, probably more accurate.