Library Coq.Logic.Classical_Pred_Set
This file is obsolete, use Classical_Pred_Type.v via Classical.v instead
Classical Predicate Logic on Set
Require
Import
Classical_Pred_Type
.
Section
Generic
.
Variable
U
:
Set
.
de Morgan laws for quantifiers
Lemma
not_all_ex_not
:
forall
P
:
U
->
Prop
,
~
(
forall
n
:
U
,
P
n
)
->
exists
n
:
U
,
~
P
n
.
Lemma
not_all_not_ex
:
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
.