Small optimization: `WSet` to avoid repeating sides of solved form inequalities. Small fix to `avl_tree`.