tuned error messsages for 'Proof' lines
tuned parser error messages

  - suppress "expecing number or letter" due to alphaNum in keyword
  - remove unnecessary try
  - more expressive message for datatypes
More expressive error message for Proof by induction

Error message for missing term in "Proof by induction" is more
intelligible.
make idParser more lenient