introduce top level command "Goal"; introduce proof token as type checkable expression for witnessed judgments
minor changes
add the rest of the judgments to the type of entries of a TTS context