IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
assoced equiv rel2 1. EquivRel x,y:. Symmetrize(u,v.u | v;x;y)
EquivRel x,y:. x ~ y
By:
Unfold `symmetrize` 1 THEN Unfold `assoced` 0 THEN Trivial
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
. Symmetrize(u,v.u | v;x;y)
EquivRel x,y: