This paper presents two approaches to primitive equality treatment in higher-order (HO) automated theorem proving: a calculus EP adapting traditional first-order (FO) paramodulation [RW69], and a calculus εRUε adapting FO RUE-Resolution [Dig79] to classical type theory, i.e., HO logic based on Church’s simply typed λ-calculus. εP and εRUε extend the extensional HO resolution approach εR [BK98a]. In order to reach Henkin completeness without the need for additional extensionality axioms both calculi employ new, positive extensionality rules analogously to the respective negative ones provided by εR that operate on unification constraints. As the extensionality rules have an intrinsic and unavoidable difference-reducing character the HO paramodulation approach loses its pure term-rewriting character. On the other hand examples demonstrate that the extensionality rules harmonise quite well with the difference-reducing HO RUE-resolution idea.