If you get a VC with an error : `a > 0 -> a > 0 && b > 0`, we should simplify this to `b>0`. The `a>0` part is guaranteed.