+theorem EM: ∀A:CProp. A ∨ ¬ A.
+(* Il comando assume è necessario perchè dimostriamo A∨¬A
+ per una A generica. *)
+assume A: CProp.
+(* Questo comando inizia a disegnare l'albero *)
+apply rule (prove (A ∨ ¬A));
+(* qui inizia l'albero, eseguite passo passo osservando come
+ si modifica l'albero. *)
+apply rule (RAA [H] (⊥)).
+apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
+ [ apply rule (discharge [H]).
+ | apply rule (⊥#e (⊥));
+ apply rule (¬#e (¬¬A) (¬A));
+ [ apply rule (¬#i [K] (⊥)).
+ apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
+ [ (*BEGIN*)apply rule (discharge [H]).(*END*)
+ | (*BEGIN*)apply rule (∨#i_r (¬A)).
+ apply rule (discharge [K]).(*END*)
+ ]
+ | (*BEGIN*)apply rule (¬#i [K] (⊥)).
+ apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
+ [ apply rule (discharge [H]).
+ | apply rule (∨#i_l (A)).
+ apply rule (discharge [K]).
+ ](*END*)
+ ]
+ ]
+qed.
+
+theorem ex1 : (C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E.
+apply rule (prove ((C∧G ⇒ E) ⇒ (¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
+(*BEGIN*)
+apply rule (⇒#i [h1] ((¬L ⇒ E∨C) ⇒ G ∨ L ⇒ ¬L ⇒ E));
+apply rule (⇒#i [h2] (G ∨ L ⇒ ¬L ⇒ E));
+apply rule (⇒#i [h3] (¬L ⇒ E));
+apply rule (⇒#i [h4] (E));
+apply rule (∨#e (G∨L) [h5] (E) [h6] (E));
+ [ apply rule (discharge [h3]);
+ | apply rule (∨#e (E∨C) [h6] (E) [h7] (E));
+ [ apply rule (⇒#e (¬L ⇒ E∨C) (¬L));
+ [ apply rule (discharge [h2]);
+ | apply rule (discharge [h4]);
+ ]
+ | apply rule (discharge [h6]);
+ | apply rule (⇒#e (C∧G ⇒ E) (C∧G));
+ [ apply rule (discharge [h1]);
+ | apply rule (∧#i (C) (G));
+ [ apply rule (discharge [h7]);
+ | apply rule (discharge [h5]);
+ ]
+ ]
+ ]
+ | apply rule (⊥#e (⊥));
+ apply rule (¬#e (¬L) (L));
+ [ apply rule (discharge [h4]);
+ | apply rule (discharge [h6]);
+ ]
+ ]
+(*END*)
+qed.
+
+theorem ex2 : (A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C.
+apply rule (prove ((A∧¬B ⇒ C) ⇒ (B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
+(*BEGIN*)
+apply rule (⇒#i [h1] ((B∧D ⇒ C) ⇒ (D ⇒ A) ⇒ D ⇒ C));
+apply rule (⇒#i [h2] ((D ⇒ A) ⇒ D ⇒ C));
+apply rule (⇒#i [h3] (D ⇒ C));
+apply rule (⇒#i [h4] (C));
+apply rule (∨#e (B∨¬B) [h5] (C) [h6] (C));
+ [ apply rule (lem 0 EM);
+ | apply rule (⇒#e (B∧D⇒C) (B∧D));
+ [ apply rule (discharge [h2]);
+ | apply rule (∧#i (B) (D));
+ [ apply rule (discharge [h5]);
+ | apply rule (discharge [h4]);
+ ]
+ ]
+ | apply rule (⇒#e (A∧¬B⇒C) (A∧¬B));
+ [ apply rule (discharge [h1]);
+ | apply rule (∧#i (A) (¬B));
+ [ apply rule (⇒#e (D⇒A) (D));
+ [ apply rule (discharge [h3]);
+ | apply rule (discharge [h4]);
+ ]
+ | apply rule (discharge [h6]);
+ ]
+ ]
+ ]
+(*END*)
+qed.
+
+(* Per dimostrare questo teorema torna comodo il lemma EM
+ dimostrato in precedenza. *)
+theorem ex3: (F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E.
+apply rule (prove ((F ⇒ G∨E) ⇒ (G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
+(*BEGIN*)
+apply rule (⇒#i [h1] ((G ⇒ ¬L∨E) ⇒ (L⇒F) ⇒ L ⇒ E));
+apply rule (⇒#i [h2] ((L⇒F) ⇒ L ⇒ E));
+apply rule (⇒#i [h3] (L ⇒ E));
+apply rule (⇒#i [h4] (E));
+apply rule (∨#e (G∨E) [h5] (E) [h6] (E));
+ [ apply rule (⇒#e (F ⇒ G∨E) (F));
+ [ apply rule (discharge [h1]);
+ | apply rule (⇒#e (L⇒F) (L));
+ [ apply rule (discharge [h3]);
+ | apply rule (discharge [h4]);
+ ]
+ ]
+ |apply rule (∨#e (¬L∨E) [h7] (E) [h8] (E));
+ [ apply rule (⇒#e (G⇒¬L∨E) (G));
+ [ apply rule (discharge [h2]);
+ | apply rule (discharge [h5]);
+ ]
+ | apply rule (⊥#e (⊥));
+ apply rule (¬#e (¬L) (L));
+ [ apply rule (discharge [h7]);
+ | apply rule (discharge [h4]);
+ ]
+ | apply rule (discharge [h8]);
+ ]
+ | apply rule (discharge [h6]);
+ ]
+(*END*)
+qed.