IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
lpath cons2 1. l : IdLnk
2. p : IdLnk List
3. lpath([l / p])
4. ||p|| = 0
destination(l) = source(hd(p))
By:
Unfold `lpath` -2 THEN InstHyp [0] -2 THEN Reduce -1 THEN NthHypEq -2
THEN
Analyze
THEN
Analyze
THEN
DVar `p'
THEN
All Reduce
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
||p|| = 0
destination(l) = source(hd(p))
