Added some facilities for defining terms and adding them to the context, and checking the type of terms in general. Also there is a "unsolved_goals" field in a context, and one can pop it to get the next unsolved goal.