helm/software/matita/library/didactic/exercises/natural_deduction.ma

   1 (* Esercizio 0
   2    ===========
   3
   4    Compilare i seguenti campi:
   5
   6    Nome1: ...
   7    Cognome1: ...
   8    Matricola1: ...
   9    Account1: ...
  10
  11    Nome2: ...
  12    Cognome2: ...
  13    Matricola2: ...
  14    Account2: ...
  15
  16 *)
  17
  18
  19 include "didactic/support/natural_deduction.ma".
  20
  21
  22
  23 theorem demorgan : ¬(A ∧ B) ⇒ ¬A ∨ ¬B.
  24
  25
  26