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

is mentioned

In prior sections: rel 1

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html