that is equivalent to term

The user must have applied one of the following tactics immediately before applying this tactic: assume, suppose, we need to prove, by just we proved,the thesis becomes, that is equivalent to.

If the tactic that was applied before this introduced a new hypothesis in the context, this tactic works on this hypothesis; otherwise, it works on the conclusion. Either way, if the term t is beta-equivalent to the term t1 on which this tactic is working (i.e. they can be reduced to a common term), t1 is changed with t. If the tactic that was applied before this tactic was that is equivalent to, and that tactic was working on a term t1, this tactic keeps working on t1.

If this tactic is working on the conclusion, a new sequent with the same hypotheses and the conclusion changed to t is opened. If this tactic is working on the last introduced hypotesis, a new sequent with the same conclusion is opened. The hypotheses of this sequent are the same, except for the one on which the tactic is working on, which is changed with t.