Module drinker Import pred;

$[raa : {X|Prop}((X->False)->False) -> X];

Goal {A:Prop}Or A (not A);
Intros A;
Refine raa;
Intros H;
Refine H;
Refine inr;
Intros P;
Refine H;
Refine inl;
Refine P;
Save tnd;

Goal {A,B:Prop}(not (And A B))->(Or (not A) (not B));
Intros A B H;
Refine raa;
Intros H1;
Refine H1;
Refine inl;
Intros a;
Refine H1;
Refine inr;
Intros b;
Refine H;
Refine pair;
Refine a;
Refine b;
Save deMorgan;

Goal {P:Set}{D:P->Prop}(not {x:P}D x)->(Exists [x:P]not (D x));
Intros;
Refine raa;
Intros;
Refine H;
Intros x;
Refine raa;
Intros;
Refine H1;
Refine existsI|?|([x:P]not (D x));
Refine x;
Refine H2;
Save deMorgan2;

[P:Set][D:P->Prop];
[sb:P];

Goal Exists [x:P](D x)->{z:P}(D z);
Intros;
Refine case|({y:P}D y)|(not ({y:P}D y));
Intros;
Refine existsI|?|([x:P](D x)->{z:P}D z);
Refine sb;
Intros;
Refine H;
Intros;
Refine existsE|?|([x:P]not (D x));
Intros;
Refine existsI|?|([x:P](D x)->{z:P}D z);
Refine a;
Intros;
Refine falseE;
Refine H1;
Refine H2;
Refine deMorgan2;
Refine H;
Refine tnd ({y:P}D y);
Save drinker;