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

Applies SUBST=L 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 right-hand-side for the left-hand-side in some wff provable

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

© 1988-99, Carnegie Mellon University.