  Proof terms are syntactic expressions that represent computations in term
rewriting. They were introduced by Meseguer and exploited by van Oostrom and de
Vrijer to study equivalence of reductions in (left-linear) first-order term
rewriting systems. We study the problem of extending the notion of proof term
to higher-order rewriting, which generalizes the first-order setting by
allowing terms with binders and higher-order substitution. In previous works
that devise proof terms for higher-order rewriting, such as Bruggink's, it has
been noted that the challenge lies in reconciling composition of proof terms
and higher-order substitution (\b{eta}-equivalence). This led Bruggink to
reject "nested" composition, other than at the outermost level. In this paper,
we propose a notion of higher-order proof term we dub rewrites that supports
nested composition. We then define two notions of equivalence on rewrites,
namely permutation equivalence and projection equivalence, and show that they
coincide. We also propose a standardization procedure, that computes a
canonical representative of the permutation equivalence class of a rewrite.
