in Term, functions to compute the variables of a term;
also, a variant of match_ that does not perform occur-check
use the non-occur-check variant of matching, and one-step substitution for Rewriting;
dramatically improve perfs.