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