IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
squash thru equiv rel11 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. a : T E(a,a)
By:
Sel 1 (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(a,a)
