A generic algorithm for pre-unification modulo beta-eta-conversion and an arbitrary subtype relation is presented. Furthermore it is shown that unification w.r.t. any subtype relation is universal.
BibTeX:
@inproceedings{Nipkow-Qian-CADE-92, author="Tobias Nipkow and Zhenyu Qian", title="Reduction and Unification in Lambda Calculi with Subtypes", booktitle="Proc.\ 11th Int.\ Conf.\ Automated Deduction",year=1992, editor="Deepak Kapur", publisher=Springer,series=LNCS,volume=607,pages="66--78"}A revised version appeared in Journal of Automated Reasoning.