Some definitions of interest.
IdLnk	Def IdLnk == IdId
	Thm* IdLnk  Type
lnk-inv	Def lnk-inv(l) == <1of(2of(l)),1of(l),2of(2of(l))>

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html