obtain id term

None.

It starts an equality chain t1 = ?, which, when concluded, will be added to hypoteses of the current sequent. It allows the user to apply the tactic = to continue the chain.

A new sequent for t1 = ? is opened, a new sequent for ? is opened, and a new sequent with the conclusion of the sequent on which this tactic was applied is opened, with H: t1 = ? added to its hypotheses. This hypotesis will be changed when the equality chain is concluded with H: t1 = tk, where tk is the last term of the equality chain. The goal for ? can be safely ignored, as it will be automatically closed when the equality chain is concluded.