Hi there, I am having a problem in rewriting using an assumption with parenthesis. For example: (* 1 *) (\exists (SA AND SB)' · SAInit AND SBInit) = ((\exists SA' · SAInit) AND (\exists SB' · SBInit)) (* |- *) \exists (SA AND SB)' · SAInit AND SBInit
The rewriting does not occur due to the parenthesis in the LHS. Does anyone know what should I do to solve this problem? Cheers, -- Artur Oliveira Gomes
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com