Well, I can think of one difference. In the iota version you have to have a story about what the iota term denotes if s is false. In the set abstraction case you don't. tf -- www.dpmms.cam.ac.uk/~tf; Home phone +64-3-348-6609 (that's a fax too!); mobile: +64-21-0580093. work +64-3-3642599