+(*DOCBEGIN
+
+La prova del teorema di dualità
+===============================
+
+Il teorema di dualità accennato a lezione dice che se due formule
+`F1` ed `F2` sono equivalenti, allora anche le formule duali lo sono.
+
+ ∀F1,F2:Formula. F1 ≡ F2 → dualize F1 ≡ dualize F2.
+
+Per dimostrare tale teorema è bene suddividere la prova in lemmi intermedi
+
+1. lemma `negate_invert`, dimostrato per induzione su F, utilizzando
+ `min_bool`
+
+ ∀F:Formula.∀v:ℕ→ℕ.[[ negate F ]]_v=[[ F ]]_(invert v).
+
+2. lemma `negate_fun`, conseguenza di `negate_invert`
+
+ ∀F,G:Formula. F ≡ G → negate F ≡ negate G.
+
+2. lemma `not_dualize_eq_negate`, dimostrato per induzione su F,
+ utilizzando `max_min` e `min_max`
+
+ ∀F:Formula. negate F ≡ FNot (dualize F)
+
+4. lemma `not_inj`, conseguenza di `sem_bool`
+
+ ∀F,G:Formula. FNot F ≡ FNot G → F ≡ G
+
+Una volta dimostrati tali lemmi la prova del teorema di dualità
+procede come di seguito:
+
+1. Assume l'ipotesi
+
+ F1 ≡ F2
+
+2. Utilizza `negate_fun` per ottenere
+
+ negate F1 ≡ negate F2
+
+3. Utilizzando due volte il lemma `not_dualize_eq_negate` e il lemma
+ `equiv_rewrite` ottiene
+
+ FNot (dualize F1) ≡ FNot (dualize F2)
+
+4. Conclude utilizzando il lemma `not_inj` per ottenere la tesi
+
+ dualize F1 ≡ dualize F2
+
+DOCEND*)
+