replace pattern with sterm

None.

It replaces the subterms of the current sequent matched by patt with the new term t. For each subterm matched by the pattern, t is disambiguated in the context of the subterm.

For each matched term t' it opens a new sequent to prove whose conclusion is t'=t.