G:(Id
), to,from:(|G|(IdLnk List)), e:Edge(G), i:|G|.
Thm* bi-graph(G;to;from)
((e 
from(i)) 
source(e) = i)L:A List, x:A. (A 
r B) (x L) (x L)T:(Id), to,from:(|T|(IdLnk List)), u:Edge(T).
Thm* bi-graph(T;to;from)
source(u) |T|T:(Id), to,from:(|T|(IdLnk List)), u:Edge(T).
Thm* bi-graph(T;to;from)
destination(u) |T|