Optimization to refinement for maximal approximations

[bmsherman]

Currently, if the lower approximation of a prop is True, then we just reduce the expression to True. Similarly, we should add the optimization such that if the lower approximation of a real is a Dyadic, then we just reduce to that dyadic.