These theorems implement abstraction and reduction for variable
binding contexts: `EVAL` converts a term `[?u] @ ?t` by
replacing the appropriate bound variable with `t` in `u` and
``demoting'' other bound variables as necessary. `BIND @ ?t`
(note the parameter) applied to `u` converts it to the form `
[?U] @ ?t` if the result `[?U]` of replacing each occurrence of
`t` with the appropriate bound variable and ``promoting'' other
bound variables as necessary is weakly stratified.

Fri Sep 5 16:28:58 MDT 1997