[Logiweb] lemma proof mismatch

[Martin Røpcke]

I get a lemma proof mismatch. In the proof I state a premise which is also 
in the lemma. I can't see what's wrong with the proof, and I believe I 
checked to see if "peano" was added all relevant places. The problem is in 
the proof of Mendelson Proposition 3.2(h)(ii):

http://www.diku.dk/~grue/logiweb/20050502/home/mrmr/peano-commutativity/fixed/body/tex/page.pdf

Can anyone help me out?

Regards,
Martin