+theorem EM: ∀A. A ∨ ¬ A.
+assume A: CProp.
+apply rule (prove (A ∨ ¬A));
+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));
+ [ apply rule (discharge [H]).
+ | apply rule (∨_i_r (¬A)).
+ apply rule (discharge [K]).
+ ]
+ | apply rule (¬_i [K] (⊥)).
+ apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+ [ apply rule (discharge [H]).
+ | apply rule (∨_i_l (A)).
+ apply rule (discharge [K]).
+ ]
+ ]
+ ]
+qed.