Nuprl Lemma : notnot_P_or_notP
[P:
]. (
(P 
(P)))
Proof
Definitions occuring in Statement :
uall: [x:A]. B[x],
prop: ,
not: A,
or: P Q
Definitions :
member: t 
T,
implies: P 
Q,
not: A,
guard: {T},
or: P Q,
prop: ,
uall: [x:A]. B[x]
Lemmas :
or_wf,
not_wf,
false_wf
\mforall{}[P:\mBbbP{}]. (\mneg{}\mneg{}(P \mvee{} (\mneg{}P)))
Date html generated:
2014_03_27-PM-01_44_46
Last ObjectModification:
2013_07_08-PM-04_04_39
Home
Index