IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Predicates for constructive properties of propositions, andlemmas characterizing how these predicates are inherited.Worthwhile sometime redoing thms for soft abstractionsin terms of the underlying hard abstractions / primitives.
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html