Permalink
Switch branches/tags
Nothing to show
Find file
Fetching contributors…
Cannot retrieve contributors at this time
55 lines (42 sloc) 822 Bytes
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;