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
(a term containing w)
(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