prove_roundoff_bound2 handles bare variable incorrectly

Ltac Automate.prove_roundoff_bound2 works incorrectly when the entire expression is just a variable.
The fix is:  replace the line 
```
   let a := constr:(rval env x) in let b := eval hnf in a in change a with b
```
with this line:
```
   let a := constr:(rval env x) in let b := eval red in a in change a with b
```
