IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
exteq prod family singleton vs intseg1121 1. a : 2. a' : 3. a'-a = 1
4. B : {a..a'}Type
5. f : i:{a..a'}B(i)
6. x : {a:}
7. f(x) B(x)
B(x) = B(a)
By:
Analyze6 THEN Analyze
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
}
Type
B(x)
B(x) = B(a)
