Nuprl - Proof: lpath cons 3

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: lpath cons 3

1. l : IdLnk
2. p : IdLnk List
3. lpath([l / p])
4.

||p|| = 0

hd(p) = lnk-inv(l)

By:	Unfold `lpath` -2 THEN InstHyp [0] -2 THEN Reduce -1 THEN NthHypEq -1 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