last fixes

diff --git a/helm/software/matita/contribs/didactic/shannon.ma b/helm/software/matita/contribs/didactic/shannon.ma
index cb42e8198bafd0887ef5caebe99612d148746156..f708c19baf8fb963ae27811ed99dccab5c0112ff 100644 (file)
--- a/helm/software/matita/contribs/didactic/shannon.ma
+++ b/helm/software/matita/contribs/didactic/shannon.ma
@@ -130,6 +130,7 @@ La libreria di Matita
 Per portare a termine l'esercitazione sono necessari i seguenti lemmi:
 
 * lemma `decidable_eq_nat` : `∀x,y.x = y ∨ x ≠ y`
+* lemma `sem_bool` : `∀F,v. [[ F ]]_v = 0 ∨ [[ F ]]_v = 1`
 * lemma `not_eq_to_eqb_false` : `∀x,y.x ≠ y → eqb x y = false`
 * lemma `eq_to_eqb_true` : `∀x,y.x = y → eqb x y = true`
 * lemma `min_1_sem` : `∀F,v.min 1 [[ F ]]_v = [[ F ]]_v`
@@ -138,7 +139,7 @@ Per portare a termine l'esercitazione sono necessari i seguenti lemmi:
 Nota su `x = y` e `eqb x y`
 ---------------------------
 
-Se vi siete mai chiasti la differenza tra `x = y` ed `eqb x y`
+Se vi siete mai chiesti la differenza tra `x = y` ed `eqb x y`
 quanto segue prova a chiarirla.
 
 Presi due numeri `x` e `y` in ℕ, dire che `x = y` significa i due numeri 
@@ -190,7 +191,7 @@ Il caso `FAtom` richiede maggiore cura. Assunto l'indice dell'atomo `n`,
 occorre utilizzare il lemma `decidable_eq_nat` per ottenere l'ipotesi
 aggiuntiva `n = x ∨ n ≠ x` (dove `x` è l'atomo su cui predica il teorema).
 Si procede per casi sull'ipotesi appena ottenuta.
-In entrambi i casi, usanto i lemmi `eq_to_eqb_true` oppure `not_eq_to_eqb_false`
+In entrambi i casi, usando i lemmi `eq_to_eqb_true` oppure `not_eq_to_eqb_false`
 si ottengolo le ipotesi aggiuntive `(eqb n x = true)` oppure `(eqb n x = false)`.
 Entrambi i casi si concludono con una catena di uguaglianze.