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:
cons
sublist
nil
T
:Type,
x
:
T
,
L
:
T
List. [
x
/
L
]
nil
False
By:
Auto THEN FwdThru
Thm*
L1
,
L2
:
T
List.
L1
L2
||
L1
||
||
L2
|| [-1]
THEN
Reduce -1
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
mb
list
1
Sections
MarkB
generic
Doc
T:Type, x:T, L:T List. [x / L] 
nil 
False T:Type, x:T, L:T List. [x / L] nil FalseL1,L2:T List. L1 L2 
||L1||
||L2|| [-1]
