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?


Artur Oliveira Gomes
Proofpower mailing list

Reply via email to