Nuprl - Proof: ring-leader1 wf

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ring-leader1 wf

loc:Id, R:(Id

), uid:(|R|

), out,in:(|R|

IdLnk).

ring(R;in;out)

Inj(|R|;

; uid)

ring-leader1(loc;R;uid;out;in)

MsgA List

By:	UnivCD THEN Unfold `ring-leader1` 0 THEN SplitOnConclITE THEN MaAuto

Generated subgoals:

None

About:

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