helm/matita/tests/andrea.ma

   1 inductive True: Prop \def
   2 I : True.
   3
   4 inductive False: Prop \def .
   5
   6 definition Not: Prop \to Prop \def
   7 \lambda A:Prop. (A \to False).
   8
   9 theorem absurd : \forall A,C:Prop. A \to Not A \to C.
  10 cut False.elim Hcut.apply H1.assumption.
  11 qed.
  12
  13 inductive And (A,B:Prop) : Prop \def
  14     conj : A \to B \to (And A B).
  15
  16 theorem proj1: \forall A,B:Prop. (And A B) \to A.
  17 intro. elim H. assumption.
  18 qed.
  19
  20 theorem proj2: \forall A,B:Prop. (And A B) \to A.
  21 intro. elim H. assumption.
  22 qed.
  23
  24 inductive Or (A,B:Prop) : Prop \def
  25      or_introl : A \to (Or A B)
  26    | or_intror : B \to (Or A B).
  27
  28 inductive ex (A:Type) (P:A \to Prop) : Prop \def
  29     ex_intro: \forall x:A. P x \to ex A P.
  30
  31 inductive ex2 (A:Type) (P,Q:A \to Prop) : Prop \def
  32     ex_intro2: \forall x:A. P x \to Q x \to ex2 A P Q.
  33
  34 inductive eq (A:Type) (x:A) : A \to Prop \def
  35     refl_equal : eq A x x.