Be careful not to let variables disappear too quickly in a proof. Once they are gone, you cannot do a proof by induction. Start your inductions before starting proofs by cases, the => method, the <=> method, or the if method.
Splitting a conjecture into separate conjuncts (using the /\ proof method) early in a proof often leads to repeating work on multiple conjuncts, for example, doing the same case analysis several times.
To keep lemmas and theorems from disappearing (because they normalize to true), make them immune. Typing either of the commands
when you begin the proof of a conjecture immunizes that conjecture (i.e., causes it to be immune once it becomes a theorem), but nothing else. Similarly, the commandsset immunity on prove ... by explicit-commands prove ... by explicit-commands make immune conjecture set immunity off resume by ... resume by ...
help keep instantiations from disappearing when they are special cases of other facts.set immunity ancestor instantiate ... in ... set immunity off
When a proof gets stuck:
Because LP automatically internormalizes facts, you may find that what you consider to be the information content of some user-supplied assertion has been ``spread out'' over several facts in the current logical system in a way that may not be easy to understand, particularly if the system contains dozens or hundreds of facts. Similarly, you may sometimes notice that LP is reducing (or has reduced) some expression in some way that you don't understand. The command show normal-form E, where E is the expression being mysteriously reduced, or where E is the original form of one side of a formula, will often be enlightening in such cases. Setting the trace-level up to 6 will show which rewrite rules are applied in the normalization.