IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
lpath cons41 1. l : IdLnk
2. lpath(nil)
3. ||nil|| = 0 destination(l) = source(hd(nil)) & hd(nil) = lnk-inv(l)
lpath([l])
By:
Unfold `lpath` 0 THEN Reduce 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
||nil|| = 0 
destination(l) = source(hd(nil)) & 
lpath([l])
