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