Yesterday's changes to sugar broke some things:
* case isn't smart enough to infer the right things in all cases yet, so
added previously existing case* for when it is necessary.
* reexport define-theorem and qed from sugar, since still used in prop.
* run is user-definable through the existing reflection features; moved
to sugar.
* define need not have special function support in curnel; moved to
sugar.
* fixed relevant documentation
