page 2  1 2 x 
We want to prove
pop (< 0 , nil >) = emptyConjunction elimination yields 3 subgoals:
And thus the main goal is proved. 
Explanation
As in the previous attempt, the first rule applied is conjunction elimination, resulting in three subgoals, with the first succeeding by circular coinduction and the second by reduction. But now the third subgoal succeeds using circular coinduction, after the lemma has been introduced. Since the proof failed on the previous page without the lemma, we know that the lemma is needed. 
