the thesis becomes P
the thesis becomes term
The provided term P must be identical to the current conclusion.
It allows the user to start a chain of reductions on the conclusion with the tactic that is equivalent to, after stating the current conclusion.
None.