In the following lemmas, we let D range over any right hand
side of a judgment, except for the chemical judgment.
Lemma 2 [Useless variable]
For any judgment of the form A |- D, and any
name x that is not free in D we have:
A |- D Û A + A' |- D
where A' is either x : s or x: s, x : " X. B.
Lemma 3 [Renaming of type variables]
Let h be a substitution on type variables. We have:
A |- D Þ h(A) |- h(D)
We say that a type scheme " X . t is more general than
" X'. t' if t' is of the form h (t) for some
substitution h replacing type and row variables by types and rows,
respectively.
This notion is also lifted to set of assumptions as follows:
A' is more general than A if A and
A' have the same domain and for each u in their domain,
A'(u) is more general than A(u).
Lemma 4 [Generalization]
If A |- D and A' is more general than A, then A' |- D.
Lemma 5 [Substitution of a name in a term]
If A + x : t |- D and A |- u : t then A |- D
{u/x}.
Similarly, if A + x : [mi : ti i Î I],
x : (l : tll Î S) |- D and
A |- y : t,
(A |- y.mi : ti) i Î I, and
(A |- y.l : tl)l Î S then A |- D{x
¬ y}.
Lemma 6 [Substitution of a class name in a term]
Let A + c : " X . z(r)BW,V |- D and
A + B |- C :: z(r)BW,V and
X Í Gen (r, B, A).
Then A |- D {c ¬ C}.