[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------] > the same idea was used by Furio Honsell about the same time to prove > SN for the Edinburgh Logical Framework. The idea was attributed to Plotkin in the JACM paper "A Framework for Defining Logics", if I recall correctly. - David.