Dear type theorists, what is the origin of the term "subject reduction"? I am of course referring to the property that if M:A and M -> N, then N:A, also known as type preservation. I can sort of see where "reduction" comes into it, but why "subject"? Thanks, -- Peter