"What is wrong in this picture?" > _+2_ : Nat2 -> Nat2 -> Nat2 > zero2 *2 m = zero2 > suc n +2 m = suc (n +2 m) -- Andreas Abel <>< Du bist der geliebte Mensch. Department of Computer Science and Engineering Chalmers and Gothenburg University, Sweden andreas.abel at gu.se http://www2.tcs.ifi.lmu.de/~abel/