PrintForm
Definitions
Lemmas
hol
list
2
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
length
cons
2
'a
:S,
l
:
'a
List,
n
:
.
||
l
|| =
n
+1
(
h
:
'a
,
l'
:
'a
List. ||
l'
|| =
n
&
l
= cons(
h
;
l'
))
By:
RewriteOfThm Thm:
hlength
cons
2
(SimpsetC [`hol_to_nuprl`;`bequal`])
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
hol
list
2
Sections
HOLlib
Doc
'a:S, l:'a List, n:
.
||l|| = n+1 
(
h:'a, l':'a List. ||l'|| = n 
