Hi there,

It doesn't look like parentheses are the problem.  It might be a problem
> with types or something else that is not visible in the pretty-printed Z
> that is stopping the LHS of he assumption matching the conclusion of the
> goal. Can you provide an example with definitions of SA etc. that can be
> run?

Yes, an example is attached here as follows.

Thanks in advance,

Artur Oliveira Gomes

Attachment: example-09-05-18.doc
Description: MS-Word document

Proofpower mailing list

Reply via email to