1. G : Id
2. to : |G|(IdLnk List)
3. from : |G|(IdLnk List)
4. e : Edge(G)
5. bi-graph(G;to;from)
  destination(e)  |G|

By:	BackThru Thm* T:(Id), to,from:(|T|(IdLnk List)), u:Edge(T). Thm* bi-graph(T;to;from)  destination(u)  |T|

None

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html