(bvule s t) abbreviates (or (bvult s t) (= s t))