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

is mentioned by

Thm* R1,R2:(TTProp). Thm* (Sym x,y:T. x R1 y)  (Sym x,y:T. x R2 y)  (Sym x,y:T. x (R1  R2) y)	[symmetric_rel_or]
Thm* R:(TTProp). (Sym x,y:T. x R y)  (Sym x,y:T. x (R^*) y)	[rel_star_symmetric]

In prior sections: rel 1

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