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