QI_TAC
bossLib.QI_TAC : tactic
Try to instantiate quantifiers with some default heuristics.
QI_TAC is short for QUANT_INSTANTIATE_TAC [std_qp].
See also
bossLib.ASM_QI_TAC,
quantHeuristicsLib.QUANT_INSTANTIATE_TAC,
quantHeuristicsLib.ASM_QUANT_INSTANTIATE_TAC