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

Applies EQUIV-IMPLICS if a support line is an equivalence.

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

If a support line is a rewrite node for an equivalence to a

conjunction, applies the equiv-implics rule.

© 1988-99, Carnegie Mellon University.