Higher-Order Unification: A structural relation between Huet's method and the one based on explicit substitutions

Higher-Order Unification: A structural relation between Huet's method and the one based on explicit substitutions