implement backward eval.  This should make normalization easier in the lemmas
some very small step forward