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

is mentioned by

Thm* P:(AAProp).  Thm* (Sym x,y:A. P(x,y))  (Sym L1,L2:A List. L1 swap adjacent[P(x,y)] L2)

[symmetric_swap_adjacent]

In prior sections: rel 1 mb nat

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