(2steps total)
PrintForm
Definitions
mb
list
1
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
iseg
weakening
T
:Type,
l
:
T
List.
l
l
By:
Unfold `iseg` 0 THEN InstConcl [nil]
Generated subgoal:
1
1.
T
: Type
2.
l
:
T
List
l
= (
l
@ nil)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
mb
list
1
Sections
MarkB
generic
Doc