4 Compilare i seguenti campi:
19 include "didactic/support/natural_deduction.ma".
23 theorem demorgan : ¬(A ∧ B) ⇒ ¬A ∨ ¬B.
24 apply rule (prove (¬(A ∧ B) ⇒ ¬A ∨ ¬B));
25 apply rule (⇒_i [H] (¬A ∨ ¬B));
26 apply rule (RAA [K] (⊥));
27 apply rule (¬_e (¬(¬A ∨ ¬B)) (¬A ∨ ¬C));
28 [ apply rule (discharge [H]).