fold reduction-kind sterm pattern

The pattern must not specify the wanted term.

First of all it locates all the subterms matched by patt. In the context of each matched subterm it disambiguates the term t and reduces it to its red normal form; then it replaces with t every occurrence of the normal form in the matched subterm.

None.