Library tutorial

Section Predicate_calculus.

Variable D : Set.
Variable R : D->D->Prop.



Variable P : D->Prop.
Variable d :D.

Lemma weird : (forall x:D, P x) -> exists a, P a.

Hypothesis EM: forall A:Prop, A\/~A.

Lemma drinker : exists x:D, P x->forall x:D, P x.

End Predicate_calculus.