Just as I gave an elimination rule for thick, so I give one for check.

The point is that every tree t has one of these forms

• put (leaf w) p

  (a term containing w)

• (thin w) |> t'

  (a term not containing w, ie some t' from a compressed variable space, thinned by a superfluous w)

The check function decides which. Its elimination rule expresses this behaviour in a readily applicable way. Let's prove it.

Next: proving checkElim | Prev: the occur check | Up: contents