Def hd(l) == Case of l; nil  "?" ; h.t  h

is mentioned by

Thm* l:IdLnk, p:IdLnk List. Thm* lpath([l / p]) Thm*  Thm* lpath(p) Thm* & (||p|| = 0    destination(l) = source(hd(p)) & hd(p) = lnk-inv(l))	[lpath_cons]
Def lconnects(p;i;j) Def == lpath(p) Def == & (||p|| = 0    i = j  Id) Def == & (||p|| = 0    i = source(hd(p)) & j = destination(last(p)))	[lconnects]

In prior sections: mb list 1 mb event system 1 list 1

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