- | apply rule (⊥_e (⊥));
- apply rule (¬_e (¬¬A) (¬A));
- [ apply rule (¬_i [K] (⊥)).
- apply rule (¬_e (¬(A ∨ ¬A)) (A ∨ ¬A));
+ | apply rule (⊥#e (⊥));
+ apply rule (¬#e (¬¬A) (¬A));
+ [ apply rule (¬#i [K] (⊥)).
+ apply rule (¬#e (¬(A ∨ ¬A)) (A ∨ ¬A));
-apply rule (⇒_i [h1] (∀x.¬ P x));
-apply rule (∀_i {l} (¬P l));
-apply rule (¬_i [h2] (⊥));
-apply rule (¬_e (¬(∃x.P x)) (∃x.P x));
+apply rule (⇒#i [h1] (∀x.¬ P x));
+apply rule (∀#i {l} (¬P l));
+apply rule (¬#i [h2] (⊥));
+apply rule (¬#e (¬(∃x.P x)) (∃x.P x));
-apply rule (⇒_i [h1] (∀x.P x ⇒ Q c));
-apply rule (∀_i {l} (P l ⇒ Q c));
-apply rule (⇒_i [h2] (Q c));
-apply rule (⇒_e ((∃x.P x) ⇒ Q c) (∃x.P x));
+apply rule (⇒#i [h1] (∀x.P x ⇒ Q c));
+apply rule (∀#i {l} (P l ⇒ Q c));
+apply rule (⇒#i [h2] (Q c));
+apply rule (⇒#e ((∃x.P x) ⇒ Q c) (∃x.P x));
- | apply rule (∃_i {y} (P y ⇒ Q c));
- apply rule (⇒_i [h4] (Q c));
- apply rule (⇒_e ((∀x.P x) ⇒ Q c) ((∀x.P x)));
+ | apply rule (∃#i {y} (P y ⇒ Q c));
+ apply rule (⇒#i [h4] (Q c));
+ apply rule (⇒#e ((∀x.P x) ⇒ Q c) ((∀x.P x)));
- | apply rule (∃_i {y} (P y ⇒ Q c));
- apply rule (⇒_i [h5] (Q c));
- apply rule (⊥_e (⊥));
- apply rule (¬_e (¬P y) (P y));
+ | apply rule (∃#i {y} (P y ⇒ Q c));
+ apply rule (⇒#i [h5] (Q c));
+ apply rule (⊥#e (⊥));
+ apply rule (¬#e (¬P y) (P y));