If our occur check succeeds, we get back the checked tree, but over
the thickened set of variables. The **ko** (`knockout') function
allows us to exploit this value.

**ko** takes a variable *w* from a set,
and a tree *t* over the set one smaller
(ie thickened at *w*): exactly the kind of tree returned
by **check**. It returns the substitution which
replaces *w* by *t* and thickens all the other variables.

The combined effect of **|>**, **ko** and **check**
is to implement the replacement of a variable by a tree which
does not contain it. Not only is the variable replaced: it is removed
from the set available, and this removal is reflected in the type
of **ko**.

Tidiness suggests that we should prove a wrapped-up version of
**thickElim** called **koElim**. Can you guess what it
says? (Hint, useful properties 1 and 2.)

Next: unification as optimisation | Prev: apply ind hyps | Up: contents

Conor's Work Page