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

If a support line is an implication, sets up a symmetric simplification

problem using the antecedent of the implication in the lemma. Then

symmetric simplification is performed.

© 1988-99, Carnegie Mellon University.