> Succ = /\a(Ln:nat(Lx:a(Lf:a->a(f(n a x f))))) Sorry the /\a shouldn't be in front : Succ = Ln:nat(/\a(Lx:a etc. Mat Matej Pfajfar St John's College, University of Cambridge, UK GPG Public Key @ http://matejpfajfar.co.uk/keys Most people are good people, the rest of us are going to run the world. -- badbytes WARNING: THIS E-MAIL ACCOUNT WILL BE DELETED ON 30/09/2002. PLEASE USE mp@cantab.net.