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

Applies SUBST=R if planned line follows by this rule from a support line.

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

If a support line is an equality, and the planned line follows from the

substituting the left-hand-side for the right-hand-side in some wff provable

from the other supports, applies Subst=R. See Pfenning's theorem 141.

© 1988-99, Carnegie Mellon University.