Re: Skip termination proofs

[Chris Warburton]

NOTE - Using 'sorry' as an exhaustiveness proof will, in cases like
destructors, give warnings like:

  ### Missing patterns in function definition:
  ### destructorp Z = undefined

This comes from the internals of the way 'function' works; it inserts
these 'undefined' values for any patterns which weren't provided
(e.g. the 'Z' pattern for predecessor in this case).

This is just a warning, so we can ignore it.