+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
+--------------------------------------------
+
+...