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* : [*m*_{i}* : t*_{i}* *^{i Î I}*],
**x* : (*l* : t_{l}^{l Î S}*) |-** D** and
**A* |-* **y* : t*,
(**A* |-* **y*.*m*_{i}* : t*_{i}*) *^{i Î I}*, and
(**A* |-* **y*.*l* : t_{l}*)*^{l Î S}* then **A* |-* D{**x*
¬ *y*}*.
*

**Lemma 6** [Substitution of a class name in a term] *
**
Let **A* + *c* : " *X* . z(r)*B*^{W,V}* |-** D** and
**A* + *B* |-* **C* :: z(r)*B*^{W,V}* and
**X* Í *Gen* (r, *B*, *A*).
Then *A* |-* D {**c* ¬ *C*}*.
*