We no longer abuse empty strings for anonymous binders. Instead, we
now have a data type for binders: a binder is either named or
anonymous.

It is based on type classes and can it be tuned by providing
instances, for example, instances can be provided to mark that
certain expressions are closed.

this makes it slightlymore annoying to use because we have to elliminate the box. one more reason to have a proof mode ;-)

We only use wp_value in the end if the resulting goal is yet
another wp. Otherwise we may not be able to do a final view
shift (as observed by Ralf).