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