Well, with git you have to know to go and look for the previous version.  With commented text you can see immediately that there's something there when looking at the source.  I thought it might be nice to remember the other proof, in case for instance in the second edition we decided to reorder things again so that this lemma comes before thm:contr-unit.  But I don't feel strongly about it.