(6steps total)
PrintForm
Definitions
Lemmas
mb
list
1
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
l
before
member
T
:Type,
L
:
T
List,
a
,
b
:
T
.
a
before
b
L
(
b
L
)
By:
Unfolds [`l_before`] 0
Generated subgoal:
1
1.
T
: Type
2.
L
:
T
List
3.
a
:
T
4.
b
:
T
5. [
a
;
b
]
L
(
b
L
)
5
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
PrintForm
Definitions
Lemmas
mb
list
1
Sections
MarkB
generic
Doc
T:Type, L:T List, a,b:T. a before b 
L 
(b L) T:Type, L:T List, a,b:T. a before b L (b L)
L
(b L)
