unfold [sterm] pattern

None.

It finds all the occurrences of t (possibly applied to arguments) in the subterms matched by patt. Then it δ-expands each occurrence, also performing β-reduction of the obtained term. If t is omitted it defaults to each subterm matched by patt.

None.