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.