added bv inequality lemmas
added bv inequality rewrite
fixed merge