IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
The 'Type{j}' type for T was necessary for proving the lemma eqvtype_wf in theory subtyping.
With 'Type{i}', the type of symmetrize was unnecessarily tied to the type of the arguments a and b.
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
