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
example-09-05-18.doc
Description: MS-Word document
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
