HoTT/book — pull request #682 by jledent (2014-06-19 13:26:44+00:00)
Title: Deleted an obsolete sentence

The variable y doesn't exist anymore, it came from a previous version where the type E(n) \to E(\suc(n)) was expressed as a product type with y : E(n)