(2steps total)
PrintForm
Definitions
hol
list
1
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
rep
list
wf
'a
:S,
l
:
'a
List. rep_list(
'a
;
l
)
(
'a
)
By:
Unfold `rep_list` 0 THEN Simp THEN StrongAuto
Generated subgoal:
1
1.
'a
: S
2.
l
:
'a
List
3.
n
:
4.
n
<
||
l
||
n
<||
l
||
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
hol
list
1
Sections
HOLlib
Doc
'a:S, l:'a List. rep_list('a;l) 
(
'a)
'a:S, l:'a List. rep_list('a;l) ('a)
||l||
n<||l||
