[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: ? about the quant rule



Mark,
   You should use (APPLY-EXTENSIONALITY) rather than the
EXTENSIONALITY lemma.  Then use (GRIND) or

   (AUTO-REWRITE-THEORY "sets[T]")
   (ASSERT)

NOTE. <TAB> E will save you some typing.

I don't know why your QUANT command failed.   I think that most people use
INST rather than QUANT now. 


Rick Butler