Def  Sym x,y:T. E(x;y) == a,b:T. E(a;b)  E(b;a)

is mentioned

In prior sections: rel 1

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html