@@ -82,9 +82,9 @@ intuitively, $\lambda^{\wedge_{i\in I}s_i\to t_i} x.e$ is a well-typed

value if for all $i{\in} I$ the hypothesis that $x$ is of type $s_i$

implies that the body $e$ has type $t_i$, that is to say, it is well

typed if $\lambda^{\wedge_{i\in I}s_i\to t_i} x.e$ has type $s_i\to

t_i$ for all $i\in I$. Every value is associated to a most specific type: the type of $c$ is $\basic c$; the type of

t_i$ for all $i\in I$. Every value is associated to a most specific type (mst): the mst of $c$ is $\basic c$; the mst of

$\lambda^{\wedge_{i\in I}s_i\to t_i} x.e$ is $\wedge_{i\in I}s_i\to t_i$; and, inductively,

the type of a pair of values is the product of the types of the

the mst of a pair of values is the product of the mst of the

values. We write $v\in t$ if $t$ is a subtype of the most specific type of $v$ (see Appendix~\ref{app:typeschemes} for the formal definition of $v\in t$ which deals with some corner cases for negated arrow types).