Fixed box unification.

TermSeq::IsSuffixOf(z) was not and should not have been is-suffix-of but
simply drop the last |n| actions from *this. The reason is that the two
action sequences may contain variables and therefore need not be equal.

Therefore it's now called TermSeq::WithoutLast(n) for some integer n.
Notice that the roles of the arguments (this and the only argument) are
now reversed.