Make sure deferred definitions get totality checked

Fixes #677. Now deferred definitions are all checked at the end of
checking a module.

Also, a minor fix for the situation where a function had no descending
or same arguments, which was getting ignored.