+ apply rule (prove (A ∨ ¬ A));
+
+ apply rule (RAA [H] ⊥);
+ apply rule (¬#e (¬¬A) (¬A));
+ [ apply rule (¬#i [H2] ⊥);
+ apply rule (¬#e (¬(A∨¬A)) (A∨¬A));
+ [ apply rule (discharge [H]);
+ | apply rule (∨#i_r (¬A));
+ apply rule (discharge [H2]);
+ ]
+ | apply rule (¬#i [H1] ⊥);
+ apply rule (¬#e (¬(A∨¬A)) (A∨¬A));
+ [ apply rule (discharge [H]);
+ | apply rule (∨#i_l A);
+ apply rule (discharge [H1]);
+ ]
+ ]
+qed.
+
+lemma ex1 : (A ⇒ E) ∨ B ⇒ A ∧ C ⇒ (E ∧ C) ∨ B.
+
+ apply rule (prove ((A⇒E)∨B⇒A∧C⇒E∧C∨B));