PrintForm
Definitions
mb
list
1
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
select
member
T
:Type,
L
:
T
List,
i
:
||
L
||. (
L
[
i
]
L
)
By:
Auto THEN Unfold `l_member` 0 THEN InstConcl [
i
]
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, i:
||L||. (L[i] 
L) T:Type, L:T List, i:||L||. (L[i] L)
