set_bind theory: revise setoid rewriting

- strengthen set_bind_subset to have the same arity
- add missing Params instance to prevent slow failures in setoid rewriting
- `Proper` instances can be proven before `set_bind_ext` via `set_solver`.
- `set_bind_ext` is then provable by set_solver directly.