IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
card prod family intseg singleton elim11 1. a : 2. a' : 3. a'-a = 1
4. {a..a'}Type
a {a:}
By:
Analyze
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
}
Type
a 
{a:
