HoTT/book — pull request #698 by mikeshulman (2014-08-01 20:50:21+00:00)
Title: first-order fix to the induction principle of V

the equalities have to be dependent to typecheck