IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
symmetrized preorder2 1. T : Type
2. R : TTProp
3. Refl(T;x,y.R(x,y))
4. Trans x,y:T. R(x,y)
Sym a,b:T. R(a,b) & R(b,a)
By:
Unfold `sym` 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T
Sym a,b:T. R(a,b) & R(b,a)
