Prover commands for evaluation and typechecking expressions

Now, the prover supports two new commands:

 * :t, :type gives the type of an expression
 * :e, :eval normalises the expression and prints the result

These work within the proof environment, so evaluating expressions that
contain references to hypotheses is allowed.

Fixes #505.