<div>
  <p>
    <kbd>prop;done</kbd> automatically applies all propositional logic rules for propositional operators <code>¬,∧,∨,→,↔</code> unfolding them as usual <b>IF</b> the resulting proof completes successfully.
  </p>
  <p>
    If this fails, use more powerful proof automation such as <kbd>auto</kbd>, real arithmetic decision procedures, or manual decompositions instead.
  </p>
</div>
