S. Agerholm, “A HOL Basis for Reasoning about Functional Programs”, BRICS, bd. 1, nr. 44, dec. 1994.