Take care to avoid duplicating redexes when reducing lambdas
Binders in values are annotated with a 'reducible' flag, which is set
to False if simplifying and the argument appears more than once.