Add missing typeclasses for twp.

Found that these were missing while playing around with changing a few wp proofs to twp proofs. This enables using iInv while proving twps.

I also added the instances for error messages, as they were also missing. A bit surprised that this was missing all this time and no one needed it.