Hi, I compiled and had the following in one of my proofs: peano imply peano x peano succ peano plus peano peano is there should have been a "y" at the end of the second line. Shouldn't "peano 'empty'" get caught as a syntax error by pyk? It compiled well but failed, of course, translating to something like: ...[ x' + peano ]... Regards, Martin