Refine unifiers

[Drup]

Currently, the handling of unifiers is a bit rough:

1. Unifier simplification simply "inlines" all the unnamed variables. It could do a bit more, like simplify alpha-conversions.
2. Unnamed variables should be given fresh names before printing.
3. The size function only counts the number of variables to be substituted, not the real size of the substitution.