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))a:T, as:T List, i:. 0<i i
||as|| [a / as][i] = as[(i-1)]| Theorem | Name |
| 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] |
| cites the following: | |
| a:T, as:T List, i:. 0<i i||as|| [a / as][i] = as[(i-1)] | [select_cons_tl] |