PrintForm
Definitions
mb
list
1
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
member
exists
T
:Type,
L
:
T
List.
L
= nil
(
x
:
T
. (
x
L
))
By:
Unfold `l_member` 0 THEN AssertBY (0<||
L
||) Easy THEN InstConcl [
L
[0];0]
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
mb
list
1
Sections
MarkB
generic
Doc
T:Type, L:T List. 
L = nil 
(
x:T. (x 
L)) T:Type, L:T List. L = nil (x:T. (x L))
