Freshen operator

[krame505]

@remexre pointed out that we should have some way to clone terms and freshen them with all new variables. This would be mostly straightforward to implement as a new overloaded operator like unify, implemented by generating mutually-recursive type-specific functions. These implementation functions would also need to pass a dictionary around containing all the variables seen so far in the term, mapped to their replacements in the new term.