Remove unnecessary partiality
Make proof search obviously total

This fixes the library in recent versions of Idris