SUBST=L-TAC : TACTICSUBST=L-TAC is a tactic.
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.
TPS documentation homepage