Agerholm, S. “A HOL Basis for Reasoning about Functional Programs”. BRICS Report Series, Vol. 1, no. 44, Dec. 1994, doi:10.7146/brics.v1i44.21598.