S. Agerholm, “A HOL Basis for Reasoning about Functional Programs”, BRICS, vol. 1, no. 44, Dec. 1994.