HoTT/HoTT — pull request #655 by mikeshulman (2014-12-28 05:29:39+00:00)
Title: complete the proof of contr_from_Empty

The proof of `contr_from_Empty` was not actually complete, but due to [bug 3890](https://coq.inria.fr/bugs/show_bug.cgi?id=3890) (and also [3632](https://coq.inria.fr/bugs/show_bug.cgi?id=3632)) nobody noticed.