Added a correctness property, which seems to have a longish counterexample, found by fairz3. Is there a simpler counterexample?

Make signature of IsInstanceOf consistent with other Expr's
Add isInstOf Constructor
Correctly handle This in instantiateType
Correctly handle This in MethodLifting when it belongs to a subtype
An extra unit test

This reverts commit c4bf3e88.

Follow-up to 3e4281d8. Uses mutable state to imitate similar other
properties of ClassDefs.

'this' can be of a subtype while MethodLifting.
MethodLifting sometimes needs to insert type casts.

Identifier fields which can be private are now private.
Identifier now inherits Ordered.
Define Undefined error, and its subclass SolverUndefinedError. Use it
mainly in solvers.