Let's close this lecture by quickly going through an example which is an example of a specific proof. We want to prove that the law of excluded middle implies Pierce's Law. So we are working in an environment where we have two propositions (two formulas) A and B, and we define two constants, LEM and Pierce, corresponding to the given formulas; we are not assuming them, we are just defining these constants. And then we want to prove the lemma, which we call LEM_Pierce, that LEM implies Pierce. First of all we want to use in the proof not just the name LEM or the name Pierce, but we want to use the formula corresponding to LEM and the formula corresponding to Pierce. So we unfold the definition. Then we try to prove this implication by the introduction rule in natural deduction, which means we try to get rid of the implications. The user enters the first five lines of the slide; the rest is the reply of Coq. Coq replies saying there is one sub-goal left to get the required proof and this sub-goal is A, to be proved in the environment where we have the excluded middle, of course, and we have also (A®B)®A. We are assuming H and H0 and we want to establish A. The last line is Coq's prompt.