IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
length tl12 1. A : Type
2. A List
3. u : A 4. v : A List
||u.v||1 ||tl((u.v))|| = ||u.v||-1
By:
AbReduce 0
Generated subgoal:
1
||v||+11 ||v|| = ||v||+1-1
Auto
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
||u.v||
1 
||tl((u.v))|| = ||u.v||-1
