AGERHOLM, S. A HOL Basis for Reasoning about Functional Programs. BRICS Report Series, v. 1, n. 44, 14 Dec. 1994.