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