[Logiweb] Naming variables in proofs

[Klaus Ebbe Grue]

> Hi logiweb at diku.dk
>
> It seems to me that sometimes it makes a difference how you name the 
> variables of your proof. For instance, I have tried to prove the following 
> lemma in the theory "system prime s" from the "peano axioms" page:
>
> For all X, A and B:  X -> A -> B    |-     X -> A     |-     X->B

I have observed the same but cannot explain it yet. It is the X which 
behaves strangely. The other metavariables seem to work fine.

Klaus