HoTT/book — pull request #620 by marcbezem (2014-01-27 15:18:13+00:00)
Title: successor made explicit in 5.3

successor made explicit in 5.3, plus some propagation