Add a stub routine for checking witnesses, accessed by such top level
commands as

	Check TS Witness : [ p : o ≡ o' : T ].

Implement the special terms @[wd_i] as variables, since we have to
substitute other terms for them, whose LF type is known to be "wexp",
and arrange for parsing them.