In particular, I started changing some lemmas in borrow.v to not
unfold everything right away. Unfolding everything right away
yields very big goals that do not fit in one screen and makes stuff
slow.