justification we proved term [( id )]

None.

If id is supplied, a logical cut on T is made. Otherwise, if T is 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.

If id is supplied, a new sequent with T as the conclusion is opened and then immediately closed using the supplied justification. A new sequent with the conclusion of the sequent on which this tactic was applied is opened, and a new hypotesis T is added to the context, with name id. If id is not supplied, no new sequents are opened.