(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
1
1
1.
T
: Type
2.
L
:
T
List
3.
a
:
T
4.
b
:
T
5. [
a
;
b
]
L
[
b
]
L
By:
Using [`
L2
',[
a
;
b
]]
(BackThru
Thm*
L1
,
L2
,
L3
:
T
List.
L1
L2
L2
L3
L1
L3
)
Generated subgoal:
1
[
b
]
[
a
;
b
]
3
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