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
null
T
:Type,
L
:
T
List,
x
:
T
. (
x
L
)
null(
L
)
By:
Auto THEN Decide null(
L
) THEN AssertBY (
(
x
L
)) Easy THEN Analyze -1
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, x:T. (x 
L) 
null(L) T:Type, L:T List, x:T. (x L) null(L)(x L)) Easy THEN Analyze -1
