HoTT/HoTT — pull request #96 by mikeshulman (2013-03-20 02:00:06+00:00)
Title: The Flattening Lemma

...along with some other helpful things I needed along the way. A couple of general lemmas are still in `Flattening.v` which ought to be put somewhere more appropriate, but I don't yet understand how they fit into the computational picture.