unfold t patt
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.