[Logiweb] Quantifier elimination leads to variable clash

[Kasper H0st Frederiksen]

I have been trying all day to prove Mendelson lemma 1.8, but i continue to 
be stopped by the logiweb diagnose error:
"Quantifier elimination leads to variable clash ...."

I am preatty shure the proof is correct, because i can "mess up" any 
one line and get a unifikation error instead, or i can remove the last 
line and get a "Lemma/Proof mismatch..." error. This must meen that I am 
using all the axioms corectly and that the conclusion matches the lemma i 
am trying to prove.

Here is my definition can anyone spot my error:



"[ intro test lemma
    index "test lemma"
    pyk   "test lemma"
    tex   "test lemma"
    end intro ]"


"[ math
   in theory system prime s
    lemma
        test lemma
    says
        all meta b indeed meta b peano imply meta b
    end lemma
    end math ]"

"[ math
      system prime s
    proof of
      test lemma
    reads
      arbitrary meta b end line
      line ell a because axiom prime a two indeed
        parenthesis meta b peano imply parenthesis parenthesis meta b peano 
imply meta b end parenthesis peano imply meta b end parenthesis end 
parenthesis
          peano imply
        parenthesis parenthesis meta b peano imply parenthesis meta b peano 
imply meta b end parenthesis end parenthesis peano imply parenthesis meta 
b peano imply meta b end parenthesis end parenthesis
      end line
      line ell b because axiom prime a one indeed
        meta b peano imply parenthesis parenthesis meta b peano imply meta 
b end parenthesis peano imply meta b end parenthesis
      end line
      line ell c because rule prime mp modus ponens ell a modus ponens ell 
b indeed
        parenthesis meta b peano imply parenthesis meta b peano imply meta 
b end parenthesis end parenthesis
          peano imply
        parenthesis meta b peano imply meta b end parenthesis
      end line
      line ell d because axiom prime a one indeed
        meta b peano imply parenthesis meta b peano imply meta b end 
parenthesis
      end line
      because rule prime mp modus ponens ell c modus ponens ell d indeed
        meta b peano imply meta b
      qed
    end math ]"


-Kasper Frederiksen