HoTT/book — pull request #625 by marcbezem (2014-01-31 12:29:31+00:00)
Title: exercise 5.9 added

Show that if we omit the constructor $\nil$ of $\lst A$ as defined on
page~\pageref{list_constructors}, the resulting inductive type is equivalent to $\emptyt$.