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