 Definition. A higher-order unifier for a pair \(\langle \bA,\bB\rangle\) of wffs is a substitution \(\theta\) for free occurrences of variables such that \(\theta \bA\) and \(\theta \bB\) have the same β-normal form. A higher-order unifier for a set of pairs of wffs is a unifier for each of the pairs in the set.