Automated Reasoning with Restricted Intensional Sets