the thesis becomes
Prev Chapter 8. Declarative Tactics Next

the thesis becomes

the thesis becomes t

Synopsis:

the thesis becomes term

Pre-condition:

The provided term t must be convertible with current sequent.

Action:

It changes the current goal to the one provided.

New sequent to prove:

None.

Prev Up Next
suppose Home we need to prove