The function RESQ_IMP_RES_TAC performs repeatedly resolution using a restricted quantified theorem. It takes a restricted quantified theorem and transforms it into an implication. This resulting theorem is used in the resolution.

Given a theorem th, the theorem-tactic RESQ_IMP_RES_TAC applies RESQ_IMP_RES_THEN repeatedly to resolve the theorem with the assumptions.

RESQ_IMP_RES_THEN, RESQ_RES_THEN, RESQ_RES_TAC, IMP_RES_THEN, IMP_RES_TAC, MATCH_MP, RES_CANON, RES_TAC, RES_THEN