Nuprl Lemma : double-neg-formation
P:
. (P 
(
P))
Proof
Definitions occuring in Statement :
prop: ,
all: x:A. B[x],
not: A,
implies: P Q
Definitions :
all: x:A. B[x],
prop: ,
implies: P Q,
not: A,
false: False,
member: t 
T,
uall: [x:A]. B[x]
Lemmas :
not_wf
\mforall{}P:\mBbbP{}. (P {}\mRightarrow{} (\mneg{}\mneg{}P))
Date html generated:
2013_03_20-AM-09_45_08
Last ObjectModification:
2013_02_25-PM-05_03_00
Home
Index