IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
spanner wf T:(Id), to,from:(|T|(IdLnk List)), f:(Edge(T)).
bi-graph(T;to;from) spanner(f;T;to;from) Prop
By:
Auto THEN Unfold `spanner` 0 THEN MaAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T:(Id
), to,from:(|T|
bi-graph(T;to;from) 
spanner(f;T;to;from) 
Prop
