Has anyone got anywhere with Types ex 6.3.4 ? I think it involves assuming the existence of an impossible T, but I'm not sure. Peter ===== Peter Taylor pjt33@cam.ac.uk