Make proof arguments to list functions implicit

This makes code much cleaner.  Fixes #1318.