[FOM] Equational Reduction of Predicate Calculus

[Harvey Friedman]

THEOREM. Let T be a recursively axiomatized set of sentences in first order
predicate calculus with equality, in a finite relational type consisting
entirely of constant and function symbols. There is a finitely axiomatized
set K of equations in many sorted first order predicate calculus with
equality, which is a conservative extension of T.

This is very classical looking. Who first proved this?

Harvey Friedman