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. ;-)


Artur Oliveira Gomes
Proofpower mailing list

Reply via email to