# [isabelle] safe for boolean equality

Hello,
I have a lemma which states the equality of two boolean values:

`lemma (in algebra) commutative: "(! a b . a * b = b * a) = ((op l->) =
``(op r->))";
`
If I use apply safe on this I get two sub-goals:
1. (! a b . a * b = b * a) ==> (op l-> ) = (op r->)
2. /\ a b . a * b = b * a

`The first sub-goal is provable, but the second is too weak. What is the
``rule for
`splitting a boolean equality in two implications.
Best regards,
Viorel Preoteasa

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*