A few more minor fixes in proof 2.2.2