prop;done automatically applies all propositional logic rules for propositional operators ¬,∧,∨,→,↔ unfolding them as usual IF the resulting proof completes successfully.

If this fails, use more powerful proof automation such as master, real arithmetic decision procedures, or manual decompositions instead.