Your file does not show what you were trying to do with 
LEMMA_T, or what you actually did, so its hard to offer much 

"lemma_tac" is easier to understand that "LEMMA_T", so you 
could try doing it with "lemma_tac" first.
(you can always collapse it down to an application of 
LEMMA_T once you have succeeded in proving the lemma using 


Proofpower mailing list

Reply via email to