G:(Id), to,from:(|G|(IdLnk List)), l:Edge(G).
  bi-graph(G;to;from)  inverse(l)  Edge(G)

By:	Auto THEN Unfold `bi-graph-inv` 0 THEN BackThru Thm* G:(Id), to,from:(|G|(IdLnk List)), l:Edge(G). Thm* bi-graph(G;to;from)  lnk-inv(l)  Edge(G)

None

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