Sometimes the justification of an inference step will refer to a lemma or a "side proof". We reserve the term "lemma" for a named proof, whose main goal has no declarations or numbered hypotheses, and which is "complete" in the sense that it has no unproved premise leaves.

Side proofs, on the other hand, can be partial proofs with any goal and can have unproved premise leaves. The simplest use of a side proof citation is to compress the side proof into a single inference from the unproven premises of the side proof to the goal of the side proof. For example, in this proof, sideproofs were introduced at two places, here and here, since the assertions at those leaves were deemed clear enough to make further proof in place distracting.

Side proofs are linked just like ordinary proofs. When proofs are browsed step-by-step, letters `a', `b', `c', etc. are used in the addresses of inference steps to indicate paths into side proofs. The first side proof cited at an inference step is addressed as `a', the second, if any, is addressed as `b', and so forth.

The print form of a proof prints the main proof followed by its side proofs in preorder traversal, numbering them consecutively. ( Example -- the two sideproofs are on successive pages.)