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

If substitution of equality can be applied to a support line, creates

a new disjunctive lemma based on the formula to which the equality can

be applied. Then symmetric simplification is used to simplify the lemma.

© 1988-99, Carnegie Mellon University.