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.