Hi Steven, >> In the translation to ZF which Andy and I am developing, such "strange >> proofs" actually caused some weird problems at some point. > > This sounds interesting :-) Is there more information on this > translation available? I hope there will be soon. Until that, please consider it as vapourware :-) Alex