IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
length nth tl1 1. A : Type
2. A List
n:{0...||nil||}. ||nth_tl(n;nil)|| = ||nil||-n
By:
(Reduce 0) THEN (Analyze 0) THEN (RecCaseSplit `nth_tl`)
Generated subgoals:
1
3. n : {0...0}
4. n0
0 = 0-n
Auto
2
3. n : {0...0}
4. 0<n ||nth_tl(n-1;nil)|| = 0-n
Auto
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
n:{0...||nil||}. ||nth_tl(n;nil)|| = ||nil||-n
0
