Hi One of you chaps mentioned the Nat data type data Nat = Zero | Succ Nat Let's have add :: Nat -> Nat -> Nat add Zero n = n add (Succ m)n = Succ (add m n) Prove add m Zero = m I'm on the verge of giving up on this. :-( Cheers Paul