subst

None.

For each premise of the form H: x = t or H: t = x where x is a local variable and t does not depend on x, the tactic rewrites H wherever x appears clearing H and x afterwards.

The one opened by the applied tactics.