ivor-0.1.5: lib/logic.tt

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

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

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

Data False : * = ;

Data True : * = 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;
refine and_intro;
fill b;
fill a;
Qed;
Freeze and_commutes;

or_commutes : (A:*)(B:*)(p:Or A B)(Or B A);
intros;
induction p;
intros;
refine or_intro_r;
fill a;
intros;
refine or_intro_l;
fill b;
Qed;
Freeze or_commutes;