Def rep_list('a;l) == <n:. if n<||l|| then l[n] else arb('a) fi ,||l||>

is mentioned by

Def abs_list == r:('a). @a:'a List. (r = rep_list('a;a))	[habs_list]
Def rep_list == l:'a List. rep_list('a;l)	[hrep_list]

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html