Roger, In the case of an existential with a schema as the > signature the witness will usually be a binding > display. So for each of your proofs you must > come up with the binding display of a witness > for your conjecture, i.e. a binding which satisfies > the body of the existential, and then offer it up > using exists-tac. Then you have to prove that > your witness does satisfy the predicate.
That is exactly what I am doing. Except for those examples, I can do it fine. I just did not included in the file few steps until the exist-tac. The problem is: only for those cases, what I choose as witness does not satisfy the predicate. I sent the file in order to see if someone could find the right witness for each of the three goals. ;-) Regards, -- Artur Oliveira Gomes
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
