The use of proof plans for transformation of functional programs by changes of data type. - J. D. C. Richardson (1996)