  We present a generalization of first-order unification to a term algebra
where variable indexing is part of the object language. We exploit variable
indexing by associating some sequences of variables ($X_0,\ X_1,\ X_2,\dots$)
with a mapping $\sigma$ whose domain is the variable sequence and whose range
consist of terms that may contain variables from the sequence. From a given
term $t$, an infinite sequence of terms may be produced by iterative
application of $\sigma$. Given a unification problem $U$ and mapping $\sigma$,
the \textit{schematic unification problem} asks whether all unification
problems $U$, $\sigma(U)$, $\sigma(\sigma(U))$, $\dots$ are unifiable. We
provide a terminating and sound algorithm. Our algorithm is \textit{complete}
if we further restrict ourselves to so-called $\infty$-stable problems. We
conjecture that this additional requirement is unnecessary for completeness.
Schematic unification is related to methods of inductive proof transformation
by resolution and inductive reasoning.
