Rob, It looks like the problem arises when the quantifiers are wrong, and is difficult to reproduce without the mod to allow non-unique quantifiers, since (at least in the example I was working with) if you get the quantifiers wrong you can prove the existential but you can't prove the unique existential.
I have made a tarfile which should reproduce the problem, but the uninformative error message may only arise if the liberalisation to allow non-unique quantification is incorporated in ProofPower. (which I was hoping for). So you may not feel motivated to address this small issue! Roger Jones _______________________________________________ Proofpower mailing list [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
