HoTT/book — pull request #675 by mikeshulman (2014-05-31 23:28:44+00:00)
Title: Rewritten pattern matching without K

This is a rephrasing of #674.