[Logiweb] Removing object quantifiers

[Frederik Eriksen]

Hi logiweb at diku.dk,

I've tried to prove the following lemma, using system S from Klaus's 
"check" page:

Lemma Tester: Pi V : (FORALL V. V=V) => V=V

'V' is a meta variable ('meta v') and  'FORALL'  is the object 
quantifier from the "check" page ('for all * indeed *'). I'm using  
Repetition and the Ded-rule in the proof, but it's not working. Any 
suggestions? (For more details about my proof, see the very bottom of 
the "eriksen/frozen" page).

Best Regards
Frederik.