change pattern with sterm

Each subterm matched by the pattern must be convertible with the term t disambiguated in the context of the matched subterm.

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.

None.