Tactic to automate some routine set theory by reduction to FOL,
using the assumptions and the theorems given.
LIBRARY
boss
DESCRIPTION
ASM_SET_TAC is identical in behaviour to SET_TAC except that
it uses the assumptions of a goal as well as the provided theorems.
FAILURE
Fails if the underlying resolution machinery (METIS_TAC) cannot
prove the goal, or the supplied theorems (and the assumptions) are not
enough for the FOL reduction.