+(*DOCBEGIN
+
+Il caso (FAtom n)
+-----------------
+
+Questo è il caso più difficile di tutta la dimostrazione.
+
+La tesi è `([[ if eqb [[ FAtom x ]]_v O then (FAtom n)[ FBot/x ] else (FAtom n[ FTop/x ]) ]]_v = [[ FAtom n ]]_ v)`
+
+Per dimostrarla è necessario utilizzare il lemma `decidable_eq_nat` per
+ottenere l'ipotesi agiuntiva `n = x ∨ n ≠ x` che chiameremo `H` e il lemma
+`sem_bool` per ottenre l'ipotesi aggiuntiva `[[ FAtom x ]]_v = 0 ∨ [[ FAtom x ]]_v = 1`
+che chiameremo `H1`.
+
+Si procede poi per casi sull'ipotesi `H`, e in ogni suo sotto caso si procede
+per casi su `H1`.
+
+Nei casi in cui è presente l'ipotesi aggiuntiva `n ≠ x` è bene
+ottenre tramite il lemma `not_eq_to_eqb_false` l'ipotesi aggiuntiva
+`eqb n x = false`.
+
+Abbiamo quindi quattro casi, in tutti si procede con un comando `conclude`:
+
+1. Caso in cui `n=x` e `[[ FAtom x ]]_v = 0`.
+
+ Utilizzando l'ipotesi `[[ FAtom x ]]_v = 0` e espandendo alcune definizioni
+ si ottiene che la parte sinistra della conclusione è
+
+ ([[ if eqb n x then FBot else (FAtom n) ]]_v)
+
+ Usando l'ipotesi `n = x`, poi il lemma `eqb_n_n` e espandendo alcune
+ definizioni si ottiene `0`. Tornando ad usare le due ipotesi
+ `n=x` e `[[ FAtom x ]]_v = 0` si ottiene una formula uguale al
+ lato destro della conclusione.
+
+2. Caso in cui `n=x` e `[[ FAtom x ]]_v = 1`.
+
+ Analogo al caso precedente.
+
+3. Caso in cui `n≠x` e `[[ FAtom x ]]_v = 0`.
+
+ Si ottiene l'ipotesi aggiuntiva `eqb n x = false` usando il lemma
+ `not_eq_to_eqb_false` insieme all'ipotesi `n ≠ x`. Usando il comando
+ conlude e l'ipotesi `[[ FAtom x ]]_v = 0`, la nuova ipotesi appena
+ ottenuta e espandendo alcune definizioni si ottiene una formula
+ uguale a quella di destra.
+
+4. Caso in cui `n≠x` e `[[ FAtom x ]]_v = 1`.
+
+ Analogo al caso precedente.
+
+### I comandi da usare
+
+* `assume ... : (...) .`
+
+ Assume una formula o un numero, ad esempio `assume n : (ℕ).` assume
+ un numero naturale `n`.
+
+* `by ..., ..., ..., we proved (...) (...).`
+
+ Permette di comporre lemmi e ipotesi per ottenere nuove ipotesi.
+ Ad esempio `by H, H1 we prove (F ≡ G) (H2).` ottiene una nuova ipotesi
+ `H2` che dice che `F ≡ G` componendo insieme `H` e `H1`.
+
+* `conclude (...) = (...) by ... .`
+
+ Il comando conclude lavora SOLO sulla parte sinistra della tesi. È il comando
+ con cui sini inizia una catena di uguaglianze. La prima formula che si
+ scrive deve essere esattamente uguale alla parte sinistra della conclusione
+ originale. Esempio `conclude ([[ FAtom x ]]_v) = ([[ FAtom n ]]_v) by H.`
+ Se la giustificazione non è un lemma o una ipotesi ma la semplice espansione
+ di una definizione, la parte `by ...` deve essere omessa.
+
+* `= (...) by ... .`
+
+ Continua un comando `conclude`, lavorando sempre sulla parte sinistra della
+ tesi.
+
+DOCEND*)