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)))

is mentioned by

Thm* p:IdLnk List, i:||p||, j:(i+1). Thm* lpath(p)  lconnects(l_interval(p;j;i);source(p[j]);source(p[i]))

[lpath-members-connected]

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