Nuprl - Proof: lpath-members-connected 1 2 1

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

1. p : IdLnk List
2. i :

||p||
3. j :

(i+1)
4. lpath(p)
5. i-j = 0

source(p[j]) = source(p[i])

By:	Subst' (i = j) 0

Generated subgoals:

None

About:

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