Removing matching on PS

This makes it less boring to modify what's in the proof state...
Use correct error function for PElabError

Fixes #1800
New way of dealing with unmatchable patterns

Any term which is not matchable, i.e. a function application or a
repeated variable on the left hand side, is automatically put in a
PHidden. The effect of elaborating PHidden t is to:

1. Delay the elaboration of 't' to the end of elaboration
2. When elaborating t, ensure that its value is already known due to
solving some other unification problem.

If something is PHidden, but not solvable by unification, elaboration
fails.
This finally fixes #323, and probably several other things.