Jon,
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
help.

## Advertising

"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
"lemma_tac").
Roger
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com