At some point, in the Vernacular we will have to prove something. And then we state if we want to prove a theorem or a lemma, as it is done in the slides. We want to prove a lemma of a given name; the content of the lemma - what has to be proved - is the type. Now the system enters into proof mode. Proving the property means to build a term of the given type. Proofs are developed by applying tactics, by top-down refinements of goals that are presented by the system. But of course the tactics are given by the user who has to use his ingenuity in order to prove the theorem. The style in which the proofs are constructed is natural deduction.

---