IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
quotient wf11 1. T : Type
2. E : TTProp
3. (a:T. E(a,a))
3. & (a,b:T. E(a,b) E(b,a))
3. & (a,b,c:T. E(a,b) E(b,c) E(a,c))
4. x : T E(x,x)
By:
BackThru 3
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T
a:T. E(a,a))
E(b,a))
E(x,x)
