+This is a not so short introduction to Matita, based on
+the formalization of the paper
+
+> Between formal topology and game theory: an
+> explicit solution for the conditions for an
+> inductive generation of formal topologies
+
+by S.Berardi and S. Valentini. The tutorial is by Enrico Tassi.
+
+The tutorial spends a considerable amount of effort in defining
+notations that resemble the ones used in the original paper. We believe
+this a important part of every formalization, not only for the aesthetic
+point of view, but also from the practical point of view. Being
+consistent allows to follow the paper in a pedantic way, and hopefully
+to make the formalization (at least the definitions and proved
+statements) readable to the author of the paper.
+
+Orienteering
+------------
+
+The graphical interface of Matita is composed of three windows:
+the script window, on the left, is where you type; the sequent
+window on the top right is where the system shows you the ongoing proof;
+the error window, on the bottom right, is where the system complains.
+On the top of the script window five buttons drive the processing of
+the proof script. From left to right the requesting the system to:
+
+- go back to the beginning of the script
+- go back one step
+- go to the current cursor position
+- advance one step
+- advance to the end of the script
+
+When the system processes a command, it locks the part of the script
+corresponding to the command, such that you cannot edit it anymore
+(without to go back). Locked parts are coloured in blue.
+
+The sequent window is hyper textual, i.e. you can click on symbols
+to jump to their definition, or switch between different notation
+for the same expression (for example, equality has two notations,
+one of them makes the type of the arguments explicit).
+
+Everywhere in the script you can use the `ncheck (term).` command to
+ask for the type a given term. If you that in the middle of a proof,
+the term is assumed to live in the current proof context (i.e. can use
+variables introduced so far).
+
+To ease the typing of mathematical symbols, the script window
+implements two unusual input facilities:
+
+- some TeX symbols can be typed using their TeX names, and are
+ automatically converted to UTF-8 characters. For a list of
+ the supported TeX names, see the menu: View ▹ TeX/UTF-8 Table.
+ Moreover some ASCII-art is understood as well, like `=>` and `->`
+ to mean double or single arrows.
+ Here we recall some of these "shortcuts":
+
+ - ∀ can be typed with `\Forall`
+ - λ can be typed with `\lambda`
+ - ≝ can be typed with `\def` or `:=`
+ - → can be typed with `to` or `->`
+
+- some symbols have variants, like the ≤ relation and ≼, ≰, ⋠.
+ The user can cycle between variants typing one of them and then
+ pressing ALT-L. Note that also letters do have variants, for
+ example W has Ω, 𝕎 and 𝐖, L has Λ, 𝕃, and 𝐋, F has Φ, …
+ Variants are listed in the aforementioned TeX/UTF-8 table.
+
+CIC (as implemented in Matita) in a nutshell
+--------------------------------------------
+
+...
+
+Type is a set equipped with the Id equality (i.e. an intensional,
+not quotiented set). We will avoid using Leibnitz equality Id,
+thus we will explicitly equip a set with an equality when needed.
+We will call this structure `setoid`. Note that we will
+attach the infix = symbols only to the equality of a setoid,
+not to Id.
+
+...
+
+We write Type[i] to mention a Type in the predicative hierarchy
+of types. To ease the comprehension we will use Type[0] for sets,
+and Type[1] for classes.
+
+For every Type[i] there is a corresponding level of predicative
+propositions CProp[i].
+
+CIC is also equipped with an impredicative sort Prop that we will not
+use in this tutorial.
+
+The standard library and the `include` command
+----------------------------------------------