Improve delaboration and pretty-printing for case

Now, the delaborator finds case expressions and converts them back to
the original. This makes :printdef work with these.
Follow instructions in comment and remove unused code