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