Nuprl Lemma : not_squash_elim
P:
. (
P 
P)
Proof
Definitions occuring in Statement :
prop: ,
all: x:A. B[x],
iff: P Q,
not: A,
squash: T
Definitions :
all: x:A. B[x],
prop: ,
iff: P Q,
not: A,
squash: T,
and: P 
Q,
implies: P Q,
rev_implies: P Q,
false: False,
member: t 
T,
true: True,
uall: [x:A]. B[x]
Lemmas :
squash_wf,
not_wf
\mforall{}P:\mBbbP{}. (\mneg{}P \mLeftarrow{}{}\mRightarrow{} \mneg{}\mdownarrow{}P)
Date html generated:
2013_03_20-AM-10_49_21
Last ObjectModification:
2013_02_25-PM-10_08_22
Home
Index