the thesis becomes
Prev Chapter 8. Declarative Tactics Next

the thesis becomes

the thesis becomes P

Synopsis:

the thesis becomes term

Pre-condition:

The provided term P must be identical to the current conclusion.

Action:

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.

New sequent to prove:

None.

Prev Up Next
that is equivalent to Home we need to prove