Using a lemma is one way of dividing up the work of a proof. We use lemmas in derivations by dividing a gap into two gaps, one with the lemma as a goal and the other with it as a further assumption to use in reaching the original goal. A rule Lemma (Lem) that does this is not safe in general, and we will use only special instances of it.

A lemma is always safe when it is entailed by the current goal. We can use this idea in reductio arguments, arguments whose goal is ⊥. Since ⊥ entails any sentence, a rule that does this, Lemma for Reductio (LFR), will be safe (though some restriction on its use is needed to insure it is progressive).

A lemma is also safe if we know we can reach it. We will use this sort of lemma only in attachment rules that add the lemma as an available but inactive resource. The first example of this sort of rule is Adjunction (Adj) which adds a conjunction when both conjuncts are already available. Although attachment rules can help us to close gaps sooner, care is needed in their use if they are to be progressive.