T:(Id
), to,from:(|T|(IdLnk List)).
Thm* bi-tree(T;to;from)
(
n:
. p:Edge(T) List. lpath(p) ||p||
n)T:(Id), to,from:(|T|(IdLnk List)), u:Edge(T).
Thm* bi-graph(T;to;from)
source(u) 
|T|n,m:, f:(nm). Inj(n; m; f) nmp:IdLnk List, i:||p||, j:(i+1).
Thm* lpath(p)
lconnects(l_interval(p;j;i);source(p[j]);source(p[i]))l:T List, i:||l||, j:(i+1). ||l_interval(l;j;i)|| = i-j 