we need to prove term [(id )]

None.

If id is provided, it applies a logical cut on T. Otherwise, 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 a new sequent with the conclusion of the sequent on which this tactic was applied is opened, with H:T added to the hypotheses.