IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
There are other types in Nuprl that we can consider first order types.
Each of these types has canonical members. For example, '' is a type with canonical memebers because there is only one representativ for 'true' and one representative for 'false'. We package this concept in the 'SQType(T)' predicate, which states that equal terms in T are also sqequal. This is used by MemCD, so that these types sre treated as first-order types.
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
'
'
