[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----] Dear Martin, I fully agree that things get more involved for F_{omega,sub,rec}. I haven't been clear enough in this repect. Is it correct that the metric approach guarantees a unique fixpoint X for every type equation X = T(X,\vec{Y}) where T(X,\vec{Y}) is not simply a variable?? If so I would withdraw all my complaints. Thomas 18-Oct-2002 13:10:34 -0300,4028;000000000000-00000000