While this might not be completely appropriate for a strictly unification-themed library, it doesn't seem completely out of place to provide Knuth-Bendix-like completion and/or elements thereof (e.g. term orderings). We're already doing some similar things here, and unification is a key element in the completion process.

Perhaps this is more appropriate for etuples, or an extension of facts in kanren.