HoTT/book — pull request #392 by Rotsor (2013-07-06 20:18:18+00:00)
Title: Lemma 11.2.2. Proof. Rename a variable to avoid shadowing.

May I suggest renaming a variable r in the proof of Lemma 11.2.2 to a different name?
It's currently shadowing an existing variable of the same type from the outer scope (the lemma statement).