A:Type, as:A List, n:{0...||as||}. ||nth_tl(n;as)|| = ||as||-n

1	1. A : Type 2. A List   n:{0...||nil||}. ||nth_tl(n;nil)|| = ||nil||-n	3 steps
2	1. A : Type 2. A List 3. u : A 4. v : A List 5. n:{0...||v||}. ||nth_tl(n;v)|| = ||v||-n   n:{0...||u.v||}. ||nth_tl(n;u.v)|| = ||u.v||-n	3 steps

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