IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
card sum family singleton elim121111 1. A : Type
2. a : A 3. B : {x:A| x = a }Type
4. (ib.ib/i,b. b) (i:{x:A| x = a }B(i))B(a)
5. i : A 6. i = a 7. B(i)
a = i {x:A| x = a }
By:
Analyze
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Type
ib.ib/i,b. b) 
(i:{x:A| x = a }
B(i))
a = i 
