IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/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 http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html