Have emacs strip trailing spaces
Remove useless cases in a proof script

They break compatibility with trunk.  As explained in
https://coq.inria.fr/bugs/show_bug.cgi?id=3718, notations in [match
goal with] were previously interpreted in the ambient scope, so [<>]
got interpreted as [nequiv_dec], which I don't think is what was
originally intended.  In trunk, [match goal with H : foo => ... end]
interpets [foo] in [type_scope] (which I specifically requested, and I
think is a good behavior).  This means that the tactic is more
powerful than it used to be, and so the script at the end doesn't work
any more.  The simplest solution is to simply strip out the code,
which is dead in 8.4.