Data And (A:*)(B:*) : * where and_intro : (a:A)(b:B)(And A B);

Data Or (A:*)(B:*) : * where
       or_intro_l : (a:A)(Or A B)
     | or_intro_r : (b:B)(Or A B);

Data Ex (A:*)(P:(a:A)*) : * where ex_intro : (x:A)(p:P x)(Ex A P);

Data False : * where ;

Data True : * where II : True ;

not = [A:*](a:A)False;

notElim = [A:*][p:not A][pp:A](p pp);

Axiom classical:(P:*)(Or P (not P));

and_commutes : (A:*)(B:*)(p:And A B)(And B A);
intros;
induction p;
intros;
split;
trivial;
trivial;
Qed;
Freeze and_commutes;

or_commutes : (A:*)(B:*)(p:Or A B)(Or B A);
intros;
induction p;
intros;
right;
trivial;
intros;
left;
trivial;
Qed;
Freeze or_commutes;

implies : ((a:*)(Or a (not a)))->
          (A:*)(B:*)(A -> B) -> (Or (not A) B);
intros;
case (X A);
intros;
right;
refine X0;
trivial;
intros;
left;
trivial;
Qed;