Updating the environment requires updating of a *dependent*
function. We take advantage of the structure of environments, in
particular that the number of storage cells can be compressed without
losing information in order to construct an update function for which
`update_lemma` is provable.

Current doesn't compile

Fri May 24 19:01:27 BST 1996