Nuprl - Proof: edge-to 2 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: edge-to 2 1 1 1

1. G : Id

2. to : |G|

(IdLnk List)
3. from : |G|

(IdLnk List)
4. Edge(G)
5. bi-graph(G;to;from)
6. x : Edge(G)
7. y : Edge(G)

Dec(x = y)

By:	AssertBY Dec(x = y) MaAuto THEN RepeatFor 4 ParallelLast THEN Fold `member` 0 THEN MaAuto

Generated subgoals:

None

About:

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