Giorgio's comment raises a question I need to ask too: What is known about subtyping algorithms for the *prenex fragment* (quantifiers outermost only) of F<: in the presence of recursive types (with or without F-bounds)? Satish