IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hd wf12 1. A : Type
2. A List
3. u : A 4. v : A List
5. ||v||1 hd(v) A 6. ||u.v||1
hd((u.v)) A
By:
Reduce 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
1 
hd(v) 
A
hd((u.v)) 
