IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
eq cons imp eq hds11 1. A : Type
2. a : A 3. b : A 4. as : A List
5. bs : A List
6. a.as = b.bs a.as = b.bs {cs:(A List)| ||cs||1 }
By:
Analyze
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
a.as = b.bs 
{cs:(A List)| ||cs||
1 }
