+The formalization uses the ng (new generation) version of Matita
+(that will be named 1.x when finally released).
+Last stable release of the "old" system is named 0.5.7; the ng system
+is coexisting with the old one in every development release
+(named "nightly builds" in the download page of Matita)
+with a version strictly greater than 0.5.7.
+
+To read this tutorial in HTML format, you need a decent browser
+equipped with a unicode capable font. Use the PDF format if some
+symbols are not displayed correctly.
+
+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 they request 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 going 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 notations
+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 do 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.
+
+The syntax of terms (and types) is the one of the λ-calculus CIC
+on which Matita is based. The main syntactical difference w.r.t.
+the usual mathematical notation is the function application, written
+`(f x y)` in place of `f(x,y)`.
+
+Pressing `F1` opens the Matita manual.
+
+CIC (as [implemented in Matita][3]) in a nutshell
+-------------------------------------------------
+
+CIC is a full and functional Pure Type System (all products do exist,
+and their sort is is determined by the target) with an impredicative sort
+Prop and a predicative sort Type. It features both dependent types and
+polymorphism like the [Calculus of Constructions][4]. Proofs and terms share
+the same syntax, and they can occur in types.
+
+The environment used for in the typing judgement can be populated with
+well typed definitions or theorems, (co)inductive types validating positivity
+conditions and recursive functions provably total by simple syntactical
+analysis (recursive calls are allowed only on structurally smaller subterms).
+Co-recursive
+functions can be defined as well, and must satisfy the dual condition, i.e.
+performing the recursive call only after having generated a constructor (a piece
+of output).
+
+The CIC λ-calculus is equipped with a pattern matching construct (match) on inductive
+types defined in the environment. This construct, together with the possibility to
+definable total recursive functions, allows to define eliminators (or constructors)
+for (co)inductive types. The λ-calculus is also equipped with explicitly typed
+local definitions (let in) that in the degenerate case work as casts (i.e.
+the type annotation `(t : T)` is implemented as `let x : T ≝ t in x`).
+
+Types are compare up to conversion. Since types may depend on terms, conversion
+involves β-reduction, δ-reduction (definition unfolding), ζ-reduction (local
+definition unfolding), ι-reduction (pattern matching simplification),
+μ-reduction (recursive function computation) and ν-reduction (co-fixpoint
+computation).
+
+Since we are going to formalize constructive and predicative mathematics
+in an intensional type theory like CIC, we try to establish some terminology.
+Type is the sort of sets equipped with the `Id` equality (i.e. an intensional,
+not quotiented set).
+
+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. The index `i` is just a label: constraints among
+universes are declared by the user. The standard library defines
+
+> Type[0] < Type[1] < Type[2]
+
+<object class="img" data="igft-CIC-universes.svg" type="image/svg+xml" width="400px"/>
+
+For every `Type[i]` there is a corresponding level of predicative
+propositions `CProp[i]` (the C initial is due to historical reasons, and
+stands for constructive, `PProp` would be more appropriate).
+A predicative proposition cannot be eliminated toward
+`Type[j]` unless it holds no computational content (i.e. it is an inductive proposition
+with 0 or 1 constructors with propositional arguments, like `Id` and `And`
+but not like `Or`).
+
+The distintion between predicative propositions and predicative data types
+is a peculirity of Matita (for example in CIC as implemented by Coq they are the
+same). The additional restriction of not allowing the elimination of a CProp
+toward a Type makes the theory of Matita minimal in the following sense:
+
+<object class="img" data="igft-minimality-CIC.svg" type="image/svg+xml" width="500px"/>
+
+Theorems proved in this setting can be reused in a classical framwork (forcing
+Matita to collapse the hierarchy of constructive propositions). Alternatively,
+one can decide to collapse predicative propositions and datatypes recovering the
+Axiom of Choice (i.e. ∃ really holds a content and can thus be eliminated to
+provide a witness for a Σ).
+
+Formalization choices
+---------------------
+
+We will avoid using `Id` (Leibniz equality),
+thus we will explicitly equip a set with an equivalence relation when needed.
+We will call this structure a _setoid_. Note that we will
+attach the infix `=` symbol only to the equality of a setoid,
+not to Id.