Reduction and unification in lambda calculi with a general notion of subtype
generic algorithm for preunification modulo \(\beta\eta\)- conversion
scientific article; zbMATH DE number 704961