+definition esempio3 ≝ (FOr (FAtom 0) (FAtom 1)).
+
+eval normalize on (esempio2 [ esempio3 / 2]).
+
+(*DOCBEGIN
+
+Il linguaggio di dimostrazione di Matita
+========================================
+
+L'ultimo esercizio richiede di scrivere una dimostrazione. Tale dimostrazione
+deve essere scritta utilizzando il linguaggio di dimostrazione di Matita.
+Tale linguaggio è composto dai seguenti comandi:
+
+* `assume nome : tipo`
+
+ Quando si deve dimostrare un tesi come `∀F : Formula.P`, il comando
+ `assume F : Formula` fissa una generica `Formula` `F` e la tesi
+ diventa `P` dove `F` è fissata.
+
+* `suppose P (nome)`
+
+ Quando si deve dimostrare una tesi come `P → Q`, il comando
+ `suppose P (Ipotesi1)` da il nome `Ipotesi1` a `P` e cambia la tesi
+ `Q`, che ora può essere dimostrata facendo riferimento all'assunzione
+ `P` tramite il nome `Ipotesi1`.
+
+* `we procede by induction on F to prove Q`
+
+ Se `F` è il nome di una (ad esempio) `Formula` precedentemente
+ assunta tramite il comando `assume`, inizia una prova per induzione su `F`.
+
+* `case name`
+
+ Nelle prove per induzione o per casi, ogni caso deve iniziare con il
+ comando `case nome`, ad esempio se si procede per induzione di una
+ formula uno dei casi sarà quello in cui la formula è `⊥`, si deve quindi
+ iniziare la sotto dimostrazione per tale caso con `case ⊥`.
+
+* `we procede by cases on x to prove Q`
+
+ Analogo a `we procede by induction on F to prove Q`
+
+* `by induction hypothesis we know P (name)`
+
+ Nei casi non base di una prova per induzione sono disponibili delle ipotesi
+ induttive, quindi la tesi è della forma `P → Q`, ed è possibile
+ dare un nome a `P` e procedere a dimostrare `Q`. Simile a `suppose`.
+
+* `the thesis becomes P`
+
+ Permette di modificare la tesi, utilizzando le definizioni (eventualmente
+ ricorsive) che vi compaiono. Ad esempio se la tesi fosse `min 3 5 = max 1 3`
+ si potrebbe usare il comando `the thesis becomes (3 = max 1 3)` in quanto
+ per definizione di minimo, il minimo tra `3` e `5` è `3`.
+
+* `by name1 we proved P (name2)`
+
+ Permette di ottenere una nuova ipotesi `P` chiamandola `name2` utilizzando
+ l'ipotesi `name1`.
+
+* `conclude (P) = (Q) by name`
+
+ Quando la tesi è della forma `P = Q`, si possono utilizzare delle ipotesi
+ della forma `A = B` riscrivendo `A` in `B` (o viceversa) in `P`. Per esempio
+ se la tesi fosse `sin π + 3 = 7 - 4` e si avesse una ipotesi `sin π = 0` dal
+ nome `H`, si potrebbe usare il comando `conclude (sin π + 3) = (0 + 3) by H`
+ per cambiare la conclusione in `0 + 3 = 7 - 4`.
+
+* `= (P) by name`
+
+ Da utilizzare in seguito a un comando `conclude` per riscrivere con altre
+ ipotesi.
+
+* `done`
+
+ Termina un caso della dimostrazione, è possibile utilizzarlo quando la tesi
+ è della forma `t = t`, ad esempio `0 = 0` oppure `v x = v x`.