Nuprl - Proof: select cons tl sq

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: select cons tl sq

T:Type, x:T, l:T List, i:

||l||. [x / l][(i+1)] ~ l[i]

By:	UnivCD THEN Unfold `select` 0 THEN Analyze THEN RW (AddrC [1] (RecUnfoldC `nth_tl`)) 0 THEN Reduce 0 THEN SplitOnConclITE THEN Try (Complete Auto) THEN Analyze

Generated subgoals:

None

About:

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