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.