# Library Coq.Logic.Classical_Pred_Type

Classical Predicate Logic on Type
Require Import Classical_Prop.
Section Generic.
Variable U : Type.
de Morgan laws for quantifiers
Lemma not_all_not_ex :
forall P:U -> Prop, ~ ( forall n:U, ~ P n ) -> exists n : U , P n.
Lemma not_all_ex_not :
forall P:U -> Prop, ~ ( forall n:U, P n ) -> exists n : U , ~ P n.
Lemma not_ex_all_not :
forall P:U -> Prop, ~ ( exists n : U , P n ) -> forall n:U, ~ P n.
Lemma not_ex_not_all :
forall P:U -> Prop, ~ ( exists n : U , ~ P n ) -> forall n:U, P n.
Lemma ex_not_not_all :
forall P:U -> Prop, (exists n : U , ~ P n) -> ~ ( forall n:U, P n ).
Lemma all_not_not_ex :
forall P:U -> Prop, (forall n:U, ~ P n) -> ~ ( exists n : U , P n ).
End Generic.