=== Help Tactic ===
A tactic is a user assistant that helps with theorem proving.

To add a new tactic, use the following syntax:

  use <tactic>

When a tactic is no longer needed, it can be removed with

  rem <tactic>

You will be notified when new expressions are suggested.
Each suggested expression will have an associated number.
Type the number to add it to the list of expressions.

If you wonder how to use a tactic, consult the manual:

  help <tactic>

use app       Find functions to apply to expressions
use debug     Print debugging representation of input
use and       Suggest useful steps for and expressions
use hooo      Suggest basic HOOO axioms
use eq        Make suggestions based on equality rules
use silence   Do not output list of tactics or expressions
use zero      Pick the 0th suggestion if there none others
