mb
list
2
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
P
:(
T
Prop). (
x
nil.
P
(
x
))
False
[l_exists_nil]
cites the following:
Thm*
x
:
T
. (
x
nil)
False
[nil_member]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb
list
2
Sections
MarkB
generic
Doc
P:(T
Prop). (
x
nil.P(x)) 
Falsex:T. (x nil) FalseP:(TProp). (xnil.P(x)) Falsex:T. (x nil) False