IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
quot elim21 1. T : Type
2. E : TTProp
3. EquivRel x,y:T. E(x,y)
4. a : T 5. b : T 6. E(a,b)
a = bx,y:T//E(x,y)
By:
Analyze
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T
a = b 
x,y:T//E(x,y)
