 Herbrand worked with this dual notion of Herbrandization, generalized to apply to non-prenex formulas as well, in order to prove Herbrand's theorem (Herbrand 1930).The resulting formula is not necessarily equivalent to the original one.As with Skolemization, which only preserves satisfiability, Herbrandization being Skolemization's dual preserves validity