IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
non neg length12 1. A : Type
2. A List
3. u : A 4. v : A List
5. ||v||0
||u.v||0
By:
AbReduce 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html