Si noti che "regola" `lem` non è una vera regola, ma una forma compatta
per rappresentare l'albero di prova del lemma che si sta riutilizzando.
-Per motivi che saranno più chiari una volta studiate logiche del primo ordine
-o di ordine superiore, i lemmi che si intende riutilizzare è bene
-che siano dimostrati astratti sugli atomi, ovvero per ogni
-atomo `A`...`Z` che compare nella formula, è bene aggiungere
-una quantificazione all'inizio della formula stessa (es. `∀A:CProp.`)
-e iniziare la dimostrazione con il comando `assume`. In tale
-modo il lemma EM può essere utilizzato sia per dimostrare
-`A ∨ ¬A` sia `B ∨ ¬B` sia `(A∨C) ∨ ¬(A∨C)` ...
+Per motivi che saranno più chiari una volta studiate logiche del
+primo ordine o di ordine superiore, i lemmi che si intende
+riutilizzare è bene che siano dimostrati astratti sugli atomi.
+Ovvero per ogni atomo `A`...`Z` che compare nella formula,
+è bene aggiungere una quantificazione all'inizio della formula stessa.
+Ad esempio scrivendo `∀A:CProp.` prima della formula `A ∨ ¬A`.
+La dimostrazione deve poi iniziare con il comando `assume`.
+
+In tale modo il lemma EM può essere utilizzato sia per dimostrare
+`A ∨ ¬A`, sia `B ∨ ¬B`, sia `(A∨C) ∨ ¬(A∨C)`, etc ...
DOCEND*)