  Higher-order unification (HOU) concerns unification of (extensions of)
$\lambda$-calculus and can be seen as an instance of equational unification
($E$-unification) modulo $\beta\eta$-equivalence of $\lambda$-terms. We study
equational unification of terms in languages with arbitrary variable binding
constructions modulo arbitrary second-order equational theories. Abstract
syntax with general variable binding and parametrised metavariables allows us
to work with arbitrary binders without committing to $\lambda$-calculus or use
inconvenient and error-prone term encodings, leading to a more flexible
framework. In this paper, we introduce $E$-unification for second-order
abstract syntax and describe a unification procedure for such problems, merging
ideas from both full HOU and general $E$-unification. We prove that the
procedure is sound and complete.
