As defined for use ETREE-NAT: is a primitive tactic.

If planned line is FALSEHOOD, and a support line is a negated existentially

quantified formula with exactly one admissible expansion, applies eneg rule.

Same as Pfenning's tactic 220.

© 1988-99, Carnegie Mellon University.